From e817a8a649477bce5c92352883d9640a99dc0006 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:33:29 -0300 Subject: [PATCH 1/8] 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 | 130 ++++++++++++- 3 files changed, 338 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 244447b22..00b3825db 100644 --- a/executor/src/tests/mod.rs +++ b/executor/src/tests/mod.rs @@ -1,5 +1,6 @@ pub mod ecsm_tests; pub mod flamegraph_tests; pub mod hint_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 592af95e8..21e21666a 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. @@ -27,6 +29,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 @@ -87,6 +118,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), v if v == HINT_SYSCALL_NUMBER => Ok(SyscallNumbers::Hint), _ => Err(()), @@ -98,6 +130,7 @@ impl TryFrom for SyscallNumbers { #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub enum Accelerator { Keccak, + KeccakAbsorb, Ecsm, } @@ -108,6 +141,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 @@ -185,11 +219,14 @@ pub fn compute_hint(hint_id: u64, in_be: &[u8; 32]) -> [u8; 32] { } } -/// Checks that a 32-byte operand does not overflow its lower 32-bit address limb: -/// `(addr mod 2^32) + max_offset < 2^32`. Tables that send an address to the memory -/// bus as a `[lo32, hi32]` pair with the per-access offset added to `lo32` alone -/// cannot represent a carry into `hi32`, so an operand straddling the limb boundary -/// makes the trace unprovable. Used by the ECSM and Hint ecalls. +/// Checks an accelerator operand's low-limb room: `(addr mod 2^32) + max_offset < 2^32`. +/// +/// Tables that send an address to the memory bus as a `[lo32, hi32]` pair model +/// per-access addresses as `base_lo + offset` with `base_hi` unchanged — they +/// cannot represent a carry into the high limb — so the whole operand must fit +/// inside its low 32-bit limb, or the trace is unprovable. `max_offset` is the +/// offset of the region's LAST byte. Used by the ECSM, Hint and keccak +/// sponge-absorb ecalls. fn addr_limb_ok(addr: u64, max_offset: u64) -> bool { (addr % LOW_LIMB) + max_offset < LOW_LIMB } @@ -517,6 +554,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 !addr_limb_ok(state_addr, KECCAK_STATE_BYTES - 1) + || !addr_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. @@ -762,6 +868,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 ff61d108e6c51de54d51a31c4ae6bfb1006eeaa9 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:35:26 -0300 Subject: [PATCH 2/8] 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 5228455ea..76cadb544 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; @@ -175,6 +179,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 f4dba13229505b08ab1373aaccac9c6104ca7974 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:51:54 -0300 Subject: [PATCH 3/8] 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 79ef4c715..52c61c3b6 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_hint_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_rc_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, hint. -pub const FIXED_TABLE_COUNT: usize = 11; +/// keccak_rc, keccak_sponge, register, ecsm, ecdas, hint. +/// +/// ⚠ 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 = 12; /// Number of chunks for each split table. /// The verifier needs this to reconstruct matching AIRs. @@ -520,6 +526,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 hint: VmAir, @@ -546,6 +553,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.hint.as_ref(), &mut traces.hint, &()), @@ -621,6 +629,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.hint.as_ref(), @@ -793,6 +802,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 hint: VmAir = Box::new(create_hint_air(proof_options)); @@ -914,6 +924,7 @@ impl VmAirs { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, hint, diff --git a/prover/src/tables/cpu.rs b/prover/src/tables/cpu.rs index fc4c2f976..f952461d0 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, @@ -236,6 +245,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 = @@ -259,6 +276,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() @@ -359,6 +379,9 @@ impl CpuOperation { commit_count, ecall_keccak, keccak_state_addr, + ecall_keccak_absorb, + keccak_absorb_state_addr, + keccak_absorb_data_addr, ecall_ecsm, ecall_hint, } 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 f1a899f56..7ba5d5c5c 100644 --- a/prover/src/tables/mod.rs +++ b/prover/src/tables/mod.rs @@ -38,6 +38,7 @@ pub mod hint; 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 29874caef..128b3a2c0 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -55,6 +55,7 @@ use super::hint; 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}; @@ -533,7 +534,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], @@ -547,6 +548,7 @@ fn collect_ops_from_cpu( Vec, Vec, Vec, + Vec, Vec, Vec, Vec, @@ -559,6 +561,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(); @@ -648,6 +651,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) = @@ -716,6 +729,7 @@ fn collect_ops_from_cpu( bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -1503,6 +1517,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) @@ -2445,8 +2581,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 { @@ -2488,7 +2622,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]; @@ -2678,6 +2827,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 } @@ -2864,6 +3074,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, @@ -2907,6 +3120,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, @@ -2968,6 +3182,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, @@ -3108,6 +3323,7 @@ fn collect_all_ops( dvrm_ops, commit_ops, keccak_ops, + keccak_sponge_ops, eq_ops, bytewise_ops, store_ops, @@ -3152,6 +3368,7 @@ fn build_traces( dvrm_ops, commit_ops, keccak_ops, + keccak_sponge_ops, eq_ops, bytewise_ops, store_ops, @@ -3243,6 +3460,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| h.add_ops(&collect_bitwise_from_hint(&hint_ops))), @@ -3502,20 +3720,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 { @@ -3542,6 +3787,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); @@ -3579,6 +3825,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); @@ -3607,6 +3854,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()); @@ -3643,6 +3891,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)] @@ -3717,6 +3966,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, hint: hint_trace, @@ -4006,6 +4256,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; @@ -4038,6 +4289,7 @@ impl Traces { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, hint, @@ -4094,6 +4346,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; } @@ -4144,6 +4397,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()); @@ -4171,6 +4425,7 @@ impl Traces { keccak, keccak_rnd, keccak_rc, + keccak_sponge, ecsm, ecdas, hint, @@ -4227,6 +4482,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; } @@ -4592,6 +4848,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4611,6 +4868,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4705,6 +4963,7 @@ impl Traces { bitwise_ops, commit_ops, keccak_ops, + keccak_sponge_ops, cpu32_ops, ecsm_ops, ecdas_ops, @@ -4720,6 +4979,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 d6a8b8608..67e29de6c 100644 --- a/prover/src/test_utils.rs +++ b/prover/src/test_utils.rs @@ -78,6 +78,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, }; @@ -996,6 +1000,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 a29a7cb49..c1434dd80 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"); check_air_device(&create_hint_air(&opts), "HINT"); diff --git a/prover/src/tests/constraint_program_tests.rs b/prover/src/tests/constraint_program_tests.rs index e227da53d..6bec8fb68 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"); check_air(&create_hint_air(&opts), "HINT"); diff --git a/prover/src/tests/constraint_set_tests_b.rs b/prover/src/tests/constraint_set_tests_b.rs index a7f68ecfd..f4998384e 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 9288cf2ac..8a8951a96 100644 --- a/prover/src/tests/mod.rs +++ b/prover/src/tests/mod.rs @@ -53,6 +53,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 bbc8d2c63..0b2cb97d0 100644 --- a/prover/src/tests/prove_elfs_tests.rs +++ b/prover/src/tests/prove_elfs_tests.rs @@ -1104,6 +1104,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 2a1311e4a8bfe7594c42e35a57737e8268587cf0 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 13:56:46 -0300 Subject: [PATCH 4/8] 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 f952461d0..baf4cbc93 100644 --- a/prover/src/tables/cpu.rs +++ b/prover/src/tables/cpu.rs @@ -246,8 +246,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 128b3a2c0..a49b4d277 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -1568,8 +1568,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; } @@ -1590,8 +1591,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); } @@ -1631,7 +1631,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); } @@ -3726,9 +3727,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 a250458ed14de4eb19143b320607351e0cd5d62b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 14:01:03 -0300 Subject: [PATCH 5/8] 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 eafb597182a626a130b76d898aa317f04a6f73b2 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 6 Aug 2026 14:03:59 -0300 Subject: [PATCH 6/8] 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] From 117c2b7615460f46cb21c82f8d6c384688661080 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 10 Aug 2026 15:04:26 -0300 Subject: [PATCH 7/8] spec(keccak): document the KECCAK_SPONGE absorb accelerator; refresh keccak specs for the seq wire-format Add spec/src/keccak_sponge.toml + spec/keccak_sponge.typ (the chip plus the block-reordering swap-attack the seq key prevents), wire the chapter into the book, and add KSPONGE to signatures.toml. Also refresh keccak.toml / keccak_round.toml, which still described the pre-seq Keccak bus after PR #912's wire-format change. Render verified (typst + shiroa); the interaction counter reports 216, matching the chip. --- spec/about_ecalls.typ | 2 +- spec/book.typ | 4 + spec/keccak_sponge.typ | 129 ++++++++++++++ spec/src/keccak.toml | 6 +- spec/src/keccak_round.toml | 9 +- spec/src/keccak_sponge.toml | 339 ++++++++++++++++++++++++++++++++++++ spec/src/signatures.toml | 14 +- 7 files changed, 496 insertions(+), 7 deletions(-) create mode 100644 spec/keccak_sponge.typ create mode 100644 spec/src/keccak_sponge.toml diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index f09db672b..b3b202811 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -32,4 +32,4 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / 93: `exit` (@halt) / -1: `SHA256` (@sha256) / -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 +/ -4: `KECCAK_ABSORB` (@sponge) \ No newline at end of file diff --git a/spec/book.typ b/spec/book.typ index 8bf8612af..8e3129fb7 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -49,6 +49,10 @@ ("commit.typ", [`COMMIT` chip], ), ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), + // Tag deliberately `sponge` rather than `keccak_sponge`: cross-reference + // resolution matches a label against chapter tags by PREFIX, so any tag + // starting with `keccak` would be captured by the chapter above. + ("keccak_sponge.typ", [`KECCAK_SPONGE` accelerator], ), )) ) ) diff --git a/spec/keccak_sponge.typ b/spec/keccak_sponge.typ new file mode 100644 index 000000000..ca53d82fd --- /dev/null +++ b/spec/keccak_sponge.typ @@ -0,0 +1,129 @@ +#import "/book.typ": book-page, aside +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + compute_nr_interactions, + render_chip_assumptions, + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_padding_table, +) + +#let config = load_config() +#let chip = load_chip("src/keccak_sponge.toml", config) + +#show: book-page(chip.name) +#let sponge = raw(chip.name) +#let keccak = `KECCAK` +#let keccak_rnd = `KECCAK_RND` + +The #keccak accelerator (@keccak) applies one permutation per `ECALL`. +Hashing a message of $ell$ bytes takes $ceil((ell + 1) / 136)$ permutations, and between them the guest must fold the next 136 bytes of message into the state itself --- seventeen loads, seventeen XORs and seventeen stores per block, all retired as ordinary VM cycles. +The #sponge accelerator absorbs that loop: one `ECALL` absorbs an entire run of whole rate blocks, at *one row per block*. + +In this VM, we assign syscall number -4 to the #sponge accelerator. Its arguments are + +/ `A0 = x10`: the address of the 200-byte state, which is updated in place, +/ `A1 = x11`: the address of $#`n` times 136$ bytes of message data, +/ `A2 = x12`: the number $#`n` > 0$ of rate blocks to absorb. + +For each block $k = 0, ..., #`n` - 1$ the accelerator XORs the block into the first seventeen lanes of the state and then applies the keccak permutation $kappa$: +$ #`state`_j <- #`state`_j xor #`block`_(k, j) "for all" j < 17, quad "then" quad #`state` <- kappa(#`state`) . $ +The eight capacity lanes are left out of the XOR. + +#aside("Padding is the caller's job")[ + This accelerator only ever sees *whole* rate blocks: the `ECALL` takes a block count, not a byte length. + A guest hashing $ell$ bytes absorbs $floor(ell / 136)$ whole blocks here and applies `pad10*1` to the remaining tail itself, pushing that one padded block through the #keccak accelerator (@keccak). + Consequently the domain separator, the final padding bit and the rate are outside this chip's trusted boundary: no constraint here mentions them, and an incorrectly padded message is a caller bug that this chip will faithfully absorb. +] + += Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) + +The #sponge chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) + +#strong("Note on rows and calls.") +A row is a *block*, not a call. +The $#`n`$ rows of one call all carry the same `timestamp` --- an `ECALL` is a single CPU cycle --- and are distinguished by `seq`, which counts $0, 1, ..., #`n` - 1$. +`μ_first` marks the row that receives the `ECALL` and reads the state out of memory; `μ_last` marks the row that writes the final state back. +A single-block call is both at once. + +#strong("Note on " + raw("state_in") + " and " + raw("block") + ".") +`state_in` is indexed as the specification's three-dimensional state, matching #keccak and #keccak_rnd, so lane $5#`y` + #`x`$ of memory is $#`state_in`_(#`x`, #`y`)$. +`block` is indexed by that same flat lane number, since the seventeen rate lanes do not form a rectangle in $(#`x`, #`y`)$. + += Assumptions +#render_chip_assumptions(chip, config) + += Constraints + +The chip takes the `ECALL` off the bus on its first row only: +#render_constraint_table(chip, config, groups: "output") + +That first row also reads the three argument registers. +Note that `A1` is read against `d`, this row's block address: `seq` is zero here (@sponge:c:first_seq_zero), so the two coincide. +#render_constraint_table(chip, config, groups: "registers") + +#strong("Addressing.") +Rather than materializing a pointer per lane, as #keccak does, the chip forms each access address as a *linear* expression $#`base`_0 + #`offset`$ over the low address word, leaving the high word untouched. +This costs no columns at all, and is faithful exactly when the low word has room for the largest offset --- which is what the executor guarantees for both regions before the call is logged. +It is also fail-closed: a base whose low word has drifted produces `MEMW` tokens for addresses no memory cell matches, so the bus fails to balance. +`s_addr` is nevertheless kept as bytes, so that the alignment of the state pointer can be checked in-chip. +#render_constraint_table(chip, config, groups: "mem") + +The reads all happen at the `ECALL`'s timestamp and the writeback one tick later. +This is what keeps every $(#`address`, #`timestamp`)$ pair unique: the writeback of the last row lands on the same 25 addresses as the state read of the first, and only the timestamp separates them. + +Absorption itself is a lookup, one per byte of the rate. +The lookup range-checks both operands and pins the result, so `xored` needs no separate range check --- and `state_in` and `block` need none either. +#render_constraint_table(chip, config, groups: "absorb") + +The permutation is delegated to the round chip #keccak_rnd (@keccak), which this chip drives exactly as the #keccak core chip does, except for the extra key discussed below: +#render_constraint_table(chip, config, groups: "round") + +Consecutive blocks of a call are tied together by a self-referential bus, in the same shape as `CNB` in @commit: every row but the last sends its result forward, and every row but the first consumes the result of its predecessor. +Alongside the state, the chain carries the call's registers and the block index, so that all of them are pinned to the values the first row read out of the registers. +#render_constraint_table(chip, config, groups: "chain") + +Finally, the flags and the block count: +#render_constraint_table(chip, config, groups: "bits") + += Why every permutation carries a key + +All $#`n`$ permutations of one call share a single `timestamp`, and the round chip echoes whatever key it receives through its twenty-four rounds. +Suppose the `KECCAK` interaction carried only $(#`timestamp`, #`round`)$, as it did before this chip existed. +Take a call of three blocks, and let a dishonest prover assign the three permutation results to the three rows in the rotated order +$ #`state_out`_0 = kappa(#`absorbed`_2), quad #`state_out`_1 = kappa(#`absorbed`_0), quad #`state_out`_2 = kappa(#`absorbed`_1) . $ +Every tuple sent on the `KECCAK` bus is still received exactly once, and every tuple received is still sent exactly once --- *the bus balances*. +The chain does not object either: it demands only that each row's `state_in` equal its predecessor's `state_out`, which this assignment satisfies. +What the guest gets back is the sponge of the same three blocks *in a different order*. +Nor does such a witness require inverting $kappa$: the prover computes $#`absorbed`_0$ from memory, then $kappa(#`absorbed`_0)$, and each remaining row's input follows from a value it already has. + +The fix is to give every permutation of a call a key of its own. +The `KECCAK` interaction carries a third scalar `seq`; #keccak_rnd passes it along its round chain untouched, exactly as it passes `timestamp`; the #keccak core chip, which runs one permutation per `ECALL`, always sends zero. +This chip sends the block index, and the block index is pinned twice over: @sponge:c:first_seq_zero anchors the first row at zero, and the chain sends `seq + 1` where it receives `seq`, so the rows of one call carry $0, 1, ..., #`n` - 1$. +A chain long enough to wrap the field would need about $2^64$ rows. +The values being distinct, the two `KECCAK` legs of block $k$ are the only ones keyed $(#`timestamp`, k)$, and the rotation above no longer balances. + +#strong("Why the rows of one call form a simple path.") +The keying argument assumes the rows of a call are what they look like: one first row, one last row, and a single chain between them. + +- There is exactly one `μ_first` row per call, because the CPU sends one `ECALL` token per `ECALL` and a second first row would have to consume it twice. +- The chain neither forks nor merges: each token is emitted once (on $#`μ` - #`μ_last`$) and consumed once (on $#`μ` - #`μ_first`$). Duplicating a link would either duplicate the `ECALL` consumption upstream, or downstream duplicate a write to one $(#`address`, #`timestamp`)$ pair, which the memory argument rejects. +- The call has exactly $#`n`$ rows: the first row reads $#`n`$ out of `A2`, the chain carries it unchanged, and the last row must satisfy @sponge:c:last_seq_is_n. Pinning the low word alone would leave the alias $#`n` + p$, which is why @sponge:c:last_n_high_zero pins the high word to zero as well; this bounds a provable call to $#`n` < 2^32$, which is vacuous, as $#`n`$ rows must physically exist in this table. +- A call can neither stop early nor run forever: a non-last row's chain token must be consumed by a successor, and a last row must satisfy @sponge:c:last_seq_is_n, so $#`n` = 0$ admits no witness at all --- as does any row count other than $#`n`$. + += Padding +The #sponge table can be padded to the next power of two with the following value assignments: +#render_chip_padding_table(chip, config) + +All-zero rows satisfy the arithmetic constraints and, having $#`μ` = #`μ_first` = #`μ_last` = 0$, contribute nothing to any bus. + += Notes/potential optimizations +- `state_out` is a full 200 columns, but the chain already carries it to the next row, where it reappears as `state_in`. A representation that shares one of the two would save 200 columns per row at the cost of a wider bus tuple. +- The eight capacity lanes are copied from `state_in` into the `KECCAK` tuple untouched. Only the seventeen rate lanes actually differ between `state_in` and `absorbed`. +- The chip could absorb the final padded block too, if the `ECALL` took a byte length rather than a block count and the padding bits were constrained in-chip. That would remove one `KECCAK` `ECALL` per hash, at the price of bringing `pad10*1` inside the trusted boundary. diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 1c3bade44..0ae5b20bd 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -92,11 +92,13 @@ name = "round" [[constraints.round]] kind = "interaction" tag = "KECCAK" -input = ["timestamp", 0, "input_state"] +input = ["timestamp", 0, 0, "input_state"] multiplicity = "μ" +ref = "keccak:c:permute_in" [[constraints.round]] kind = "interaction" tag = "KECCAK" -input = ["timestamp", 24, "output_state"] +input = ["timestamp", 24, 0, "output_state"] multiplicity = ["-", "μ"] +ref = "keccak:c:permute_out" diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 6ee05e29a..856571578 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -11,6 +11,11 @@ name = "round" type = "BaseField" desc = "index of the permutation round" +[[variables.input]] +name = "seq" +type = "BaseField" +desc = "index of the permutation within its `ECALL` (0 for the `KECCAK` core chip; the rate-block index for `KECCAK_SPONGE`), carried through untouched like `timestamp`" + [[variables.input]] name = "start" type = [[["Byte", 8], 5], 5] @@ -170,13 +175,13 @@ name = "io" [[constraints.io]] kind = "interaction" tag = "KECCAK" -input = ["timestamp", "round", "start"] +input = ["timestamp", "round", "seq", "start"] multiplicity = ["-", "μ"] [[constraints.io]] kind = "interaction" tag = "KECCAK" -input = ["timestamp", ["+", "round", 1], "out"] +input = ["timestamp", ["+", "round", 1], "seq", "out"] multiplicity = "μ" [[constraints.io]] diff --git a/spec/src/keccak_sponge.toml b/spec/src/keccak_sponge.toml new file mode 100644 index 000000000..d93aaee49 --- /dev/null +++ b/spec/src/keccak_sponge.toml @@ -0,0 +1,339 @@ +name = "KECCAK_SPONGE" + +# ============================================================================= +# Variables +# ============================================================================= + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp of the `ECALL` that started this absorb call; shared by every block of the call" +pad = 0 + +[[variables.input]] +name = "seq" +type = "BaseField" +desc = "index of this block within the call, counting from 0" +pad = 0 + +[[variables.input]] +name = "n" +type = "DWordWL" +desc = "number of rate blocks absorbed by this call (register `A2 = x12`)" +pad = 0 + +[[variables.input]] +name = "s_addr" +type = "DWordBL" +desc = "address of the first byte of the 200-byte state (register `A0 = x10`)" +pad = 0 + +[[variables.input]] +name = "d" +type = "DWordWL" +desc = "address of the first byte of *this* block: $#`data_ptr` + 136 dot #`seq`$" +pad = 0 + +[[variables.input]] +name = "state_in" +type = [[["Byte", 8], 5], 5] +desc = "the running sponge state entering this block" +pad = 0 + +[[variables.input]] +name = "block" +type = [["Byte", 8], 17] +desc = "the 136 message bytes of this block, as 17 little-endian lanes" +pad = 0 + +[[variables.output]] +name = "state_out" +type = [[["Byte", 8], 5], 5] +desc = "the running sponge state leaving this block: $kappa(#`absorbed`)$" +pad = 0 + +[[variables.auxiliary]] +name = "xored" +type = [["Byte", 8], 17] +desc = "$#`state_in` xor #`block`$ over the rate region" +pad = 0 + +[[variables.auxiliary]] +name = "μ_first" +type = "Bit" +desc = "whether this is the first block of the call (the row that receives the `ECALL`)" +pad = 0 + +[[variables.auxiliary]] +name = "μ_last" +type = "Bit" +desc = "whether this is the last block of the call (the row that writes the state back)" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[variables.virtual]] +name = "s_lo" +type = "Word" +desc = "the low address word of `s_addr`" +def = {poly = ["+", + ["idx", "s_addr", 0], + ["*", ["^", 2, 8], ["idx", "s_addr", 1]], + ["*", ["^", 2, 16], ["idx", "s_addr", 2]], + ["*", ["^", 2, 24], ["idx", "s_addr", 3]]]} + +[[variables.virtual]] +name = "s_hi" +type = "Word" +desc = "the high address word of `s_addr`" +def = {poly = ["+", + ["idx", "s_addr", 4], + ["*", ["^", 2, 8], ["idx", "s_addr", 5]], + ["*", ["^", 2, 16], ["idx", "s_addr", 6]], + ["*", ["^", 2, 24], ["idx", "s_addr", 7]]]} + +[[variables.virtual]] +name = "absorbed" +type = [[["Byte", 8], 5], 5] +desc = "the state handed to the permutation: `xored` on the 17 rate lanes, `state_in` on the 8 capacity lanes" +def = {polys = [ + {iters = [["x", 0, 4], ["y", 0, 2], ["z", 0, 7]], poly = ["idx", ["idx", "xored", ["+", ["*", 5, "y"], "x"]], "z"]}, + {iters = [["x", 0, 1], ["y", 3], ["z", 0, 7]], poly = ["idx", ["idx", "xored", ["+", ["*", 5, "y"], "x"]], "z"]}, + {iters = [["x", 2, 4], ["y", 3], ["z", 0, 7]], poly = ["idx", ["idx", ["idx", "state_in", "x"], "y"], "z"]}, + {iters = [["x", 0, 4], ["y", 4], ["z", 0, 7]], poly = ["idx", ["idx", ["idx", "state_in", "x"], "y"], "z"]}, +]} + +# ============================================================================= +# Assumptions +# +# These are guarantees the *executor* enforces before an absorb call is ever +# logged; a program violating one of them traps instead of producing a trace. +# The chip does not re-derive them, so they are part of its trusted boundary. +# ============================================================================= + +[[assumptions]] +desc = "$#`n` > 0$: an absorb call has at least one rate block" + +[[assumptions]] +desc = "$#`s_addr` mod 8 = 0$ and $#`d` mod 8 = 0$ on the first row: both pointers are lane-aligned" + +[[assumptions]] +desc = "the *last* byte of each region --- $#`s_addr` + 199$ and $#`d` + 136#`n` - 1$ --- neither overflows $2^64$ nor its own low address word. The chip forms per-access addresses as $#`base`_0 + #`offset`$ with $#`base`_1$ untouched, which is only faithful when the low word has the room; a prover that lies here produces `MEMW` tokens no memory cell can match, so the failure is closed rather than silent" + +[[assumptions]] +desc = "the state region and the message region are disjoint. Every read of this call happens at one timestamp, so an overlap would put two accesses on a single $(#`address`, #`timestamp`)$ pair, which the memory argument cannot order" + +[[assumptions]] +desc = "the message consists of *whole* rate blocks: `pad10*1` is applied by the caller, which sends the final, partial block through the `KECCAK` accelerator instead (@keccak). Nothing in this chip depends on, or checks, the padding" + +# ============================================================================= +# Constraints +# ============================================================================= + +[[constraint_groups]] +name = "output" + +# ECALL -4, i.e. 2^64 - 4 read as an unsigned 64-bit value. +[[constraints.output]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["cast", ["-", ["^", 2, 64], 4], "DWordWL"]] +multiplicity = ["-", "μ_first"] +ref = "sponge:c:receive_ecall" + +[[constraint_groups]] +name = "registers" + +[[constraints.registers]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", "s_lo", "s_hi", 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", "s_lo", "s_hi", 0, 0, 0, 0, 0, 0] +multiplicity = "μ_first" +ref = "sponge:c:read_state_ptr" + +[[constraints.registers]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 11], "DWordWL"], ["arr", ["idx", "d", 0], ["idx", "d", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", "d", 0], ["idx", "d", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "μ_first" +ref = "sponge:c:read_data_ptr" + +[[constraints.registers]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 12], "DWordWL"], ["arr", ["idx", "n", 0], ["idx", "n", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", "n", 0], ["idx", "n", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "μ_first" +ref = "sponge:c:read_n_blocks" + +[[constraint_groups]] +name = "mem" + +# Alignment of the state pointer: its low byte is a multiple of 8. +[[constraints.mem]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "AND"], ["idx", "s_addr", 0], 7] +output = 0 +multiplicity = "μ" +ref = "sponge:c:state_ptr_alignment" + +# `s_addr`'s bytes feed the linear address recombines `s_lo`/`s_hi`, so they +# need explicit range checks: without them a prover could encode non-byte +# values that leave `s_lo`/`s_hi` (and hence every MEMW tuple) intact while +# dodging the alignment lookup above. +[[constraints.mem]] +kind = "interaction" +tag = "ARE_BYTES" +input = [["idx", "s_addr", ["*", 2, "i"]], ["idx", "s_addr", ["+", ["*", 2, "i"], 1]]] +iter = ["i", 0, 3] +multiplicity = "μ" +ref = "sponge:c:range_s_addr" + +# The pre-call state is read lane by lane, at the ECALL's timestamp, on the +# first row only. Pure reads: the value read is written back unchanged. +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [0, ["arr", ["+", "s_lo", ["*", 8, ["+", ["*", 5, "y"], "x"]]], "s_hi"], ["idx", ["idx", "state_in", "x"], "y"], "timestamp", 0, 0, 1] +output = ["idx", ["idx", "state_in", "x"], "y"] +iters = [["x", 0, 4], ["y", 0, 4]] +multiplicity = "μ_first" +ref = "sponge:c:read_state" + +# Every row reads its own 17 message lanes, also at the ECALL's timestamp. +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [0, ["arr", ["+", ["idx", "d", 0], ["*", 8, "j"]], ["idx", "d", 1]], ["idx", "block", "j"], "timestamp", 0, 0, 1] +output = ["idx", "block", "j"] +iter = ["j", 0, 16] +multiplicity = "μ" +ref = "sponge:c:read_block" + +# The final state is written back on the last row, one timestamp later, so +# that no (address, timestamp) pair carries two accesses. +[[constraints.mem]] +kind = "interaction" +tag = "MEMW" +input = [0, ["arr", ["+", "s_lo", ["*", 8, ["+", ["*", 5, "y"], "x"]]], "s_hi"], ["idx", ["idx", "state_out", "x"], "y"], ["arr", ["+", ["idx", "timestamp", 0], 1], ["idx", "timestamp", 1]], 0, 0, 1] +iters = [["x", 0, 4], ["y", 0, 4]] +multiplicity = "μ_last" +ref = "sponge:c:write_state" + +[[constraint_groups]] +name = "absorb" + +# The message is XORed into the 17 rate lanes, lane `5y + x` of the state +# against lane `5y + x` of the block. The lookup range-checks both operands +# and pins the result, so `xored` needs no separate range check. +[[constraints.absorb]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "state_in", "x"], "y"], "z"], ["idx", ["idx", "block", ["+", ["*", 5, "y"], "x"]], "z"]] +output = ["idx", ["idx", "xored", ["+", ["*", 5, "y"], "x"]], "z"] +iters = [["x", 0, 4], ["y", 0, 2], ["z", 0, 7]] +multiplicity = "μ" +ref = "sponge:c:absorb_xor" + +[[constraints.absorb]] +kind = "interaction" +tag = "BYTE_ALU" +input = [["opsel", "XOR"], ["idx", ["idx", ["idx", "state_in", "x"], "y"], "z"], ["idx", ["idx", "block", ["+", ["*", 5, "y"], "x"]], "z"]] +output = ["idx", ["idx", "xored", ["+", ["*", 5, "y"], "x"]], "z"] +iters = [["x", 0, 1], ["y", 3, 3], ["z", 0, 7]] +multiplicity = "μ" +ref = "sponge:c:absorb_xor_tail" + +[[constraint_groups]] +name = "round" + +# The permutation is delegated to KECCAK_RND. Both legs carry `seq`, so every +# permutation of this call has a key of its own — see the chapter text. +[[constraints.round]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", 0, "seq", "absorbed"] +multiplicity = "μ" +ref = "sponge:c:permute_in" + +[[constraints.round]] +kind = "interaction" +tag = "KECCAK" +input = ["timestamp", 24, "seq", "state_out"] +multiplicity = ["-", "μ"] +ref = "sponge:c:permute_out" + +[[constraint_groups]] +name = "chain" + +# Row `k` hands the permuted state, the call's registers and the next block +# index to row `k + 1`. +[[constraints.chain]] +kind = "interaction" +tag = "KSPONGE" +input = ["timestamp", ["+", "seq", 1], "n", ["arr", "s_lo", "s_hi"], ["arr", ["+", ["idx", "d", 0], 136], ["idx", "d", 1]], "state_out"] +multiplicity = ["-", "μ", "μ_last"] +ref = "sponge:c:send_chain" + +[[constraints.chain]] +kind = "interaction" +tag = "KSPONGE" +input = ["timestamp", "seq", "n", ["arr", "s_lo", "s_hi"], "d", "state_in"] +multiplicity = ["-", ["-", "μ", "μ_first"]] +ref = "sponge:c:receive_chain" + +[[constraint_groups]] +name = "bits" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["μ"] +ref = "sponge:c:range_mu" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["μ_first"] +ref = "sponge:c:range_mu_first" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["μ_last"] +ref = "sponge:c:range_mu_last" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`μ_first` + #`μ_last` => #`μ` = 1$" +desc = "a bookend row is a real row; a single-block call is both bookends at once" +poly = ["*", ["+", "μ_first", "μ_last"], ["not", "μ"]] +ref = "sponge:c:bookends_imply_mu" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`μ_first` => #`seq` = 0$" +desc = "a call's chain is anchored at block 0; together with the chain increment this pins `seq` to $0, 1, ..., n-1$ and gives every permutation of the call a distinct key" +poly = ["*", "μ_first", "seq"] +ref = "sponge:c:first_seq_zero" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`μ_last` => #`n`_0 = #`seq` + 1$" +desc = "the call spans exactly `n` rows" +poly = ["*", "μ_last", ["-", ["idx", "n", 0], "seq", 1]] +ref = "sponge:c:last_seq_is_n" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`μ_last` => #`n`_1 = 0$" +desc = "pinning the *words* of `n`, rather than the recombined value, closes the alias $#`n` + p$: a register holding $#`n` + p$ has $#`n`_1 = 2^32 - 1 != 0$" +poly = ["*", "μ_last", ["idx", "n", 1]] +ref = "sponge:c:last_n_high_zero" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 6ea23bb9e..56c4b8c01 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -198,11 +198,21 @@ kind = "interaction" input = ["Word", "Byte", "Byte", "Byte", "Bit"] output = "Word" -# Keccak communication between rounds +# Keccak communication between rounds. +# `seq` distinguishes permutations that share one ECALL timestamp: the KECCAK +# core chip runs a single permutation per ECALL and always sends 0, while +# KECCAK_SPONGE sends the index of the rate block it is absorbing. [[signatures]] tag = "KECCAK" kind = "interaction" -input = ["DWordWL", "BaseField", [[["Byte", 8], 5], 5]] +input = ["DWordWL", "BaseField", "BaseField", [[["Byte", 8], 5], 5]] + +# KECCAK_SPONGE's self-referential block chain: +# KSPONGE[timestamp, seq, n, state_ptr, block_ptr, state] +[[signatures]] +tag = "KSPONGE" +kind = "interaction" +input = ["DWordWL", "BaseField", "DWordWL", "DWordWL", "DWordWL", [[["Byte", 8], 5], 5]] # Keccak round constants [[signatures]] From 67fdfe926451b7bdaed03cbade9b8dc33be92204 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Mon, 10 Aug 2026 15:55:45 -0300 Subject: [PATCH 8/8] feat(ethrex,syscalls): route guest keccak through the KECCAK_SPONGE accelerator (default on) Wire crypto/ethrex-crypto's sponge to absorb whole rate blocks via keccak_absorb_blocks (ECALL -4), with the pad10*1 tail through the classic per-permutation syscall -- the composition the formal check verified (E1, 417 lengths, 0 mismatches). Also wire the syscalls Keccak256 path (the recursion-verifier chain; inert for ethrex). Feature keccak-sponge-accel is declared in the syscalls / ethrex-crypto / ethrex-guest manifests and defaults ON at the guest, so `make ethrex.elf` builds the accelerated ELF (a nosponge Makefile variant builds the plain one for a local A/B). A host differential confirms accelerated == software == ethrex's reference across the block-boundary length sweep. Purpose: let /bench exercise the accelerator on a real block. --- Makefile | 21 +++ crypto/ethrex-crypto/Cargo.toml | 19 +++ crypto/ethrex-crypto/src/lib.rs | 81 +++++++++- .../ethrex-crypto/src/tests/keccak_tests.rs | 65 ++++++++ executor/programs/rust/ethrex/Cargo.toml | 27 ++++ syscalls/Cargo.toml | 8 + syscalls/src/keccak.rs | 141 ++++++++++++++++++ 7 files changed, 358 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index a4b05b507..06311f19f 100644 --- a/Makefile +++ b/Makefile @@ -217,6 +217,27 @@ endef $(RUST_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RUST_ARTIFACTS_DIR) $(call build_guest_elf,$(RUST_PROGRAMS_DIR)/$*,$*) +# Plain-software-sponge ethrex guest, for a local A/B against the default one. +# +# The ethrex guest hashes on the KECCAK_SPONGE absorb accelerator BY DEFAULT +# (see its Cargo.toml), because /bench builds the workload with a plain +# `make .../ethrex.elf` and proves whatever that contains — an accelerator +# behind a non-default feature would be invisible to it. This rule builds the +# other side of the comparison. +# +# Unlike the recursion presets below, the variant cannot be selected with a +# second `required-features`-gated [[bin]]: cargo gates a bin on a feature being +# ON, never OFF, and this axis is `--no-default-features`. So both variants come +# from the one `ethrex` bin and land on the same +# shared_target/.../release/ethrex path — build them SEQUENTIALLY (each recipe +# copies to its own $@ before the next cargo run can overwrite it), and expect +# cargo to rebuild the crate when switching, since the feature set changes. +# +# An explicit rule beats the pattern rule above, which would otherwise go +# looking for a crate directory named `ethrex-nosponge`. +$(RUST_ARTIFACTS_DIR)/ethrex-nosponge.elf: FORCE | prepare-sysroot $(RUST_ARTIFACTS_DIR) + $(call build_guest_elf,$(RUST_PROGRAMS_DIR)/ethrex,ethrex,--no-default-features) + # Compile rust benches (64-bit) $(BENCH_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(BENCH_ARTIFACTS_DIR) $(call build_guest_elf,$(BENCH_PROGRAMS_DIR)/$*,$*) diff --git a/crypto/ethrex-crypto/Cargo.toml b/crypto/ethrex-crypto/Cargo.toml index ea6c91074..249bfba80 100644 --- a/crypto/ethrex-crypto/Cargo.toml +++ b/crypto/ethrex-crypto/Cargo.toml @@ -14,6 +14,25 @@ license = "MIT OR Apache-2.0" # changes don't require an ethrex PR — the guest just constructs and injects # `LambdaVmEcsmCrypto`. +[features] +default = [] +# Route the whole 136-byte keccak rate blocks of `Crypto::keccak256` through +# the KECCAK_SPONGE absorb accelerator (ECALL -4) instead of XOR-ing them into +# the state in guest software; the padded tail stays on `keccak_permute`. The +# digests are identical either way. +# +# Off at this level, ON by default at the guest crate, so `make ethrex.elf` +# (which is what /bench builds) produces an accelerated ELF while +# `--no-default-features` still builds the plain one for a local A/B. +# +# The forward to `lambda-vm-syscalls/keccak-sponge-accel` is a no-op for this +# crate's own sponge (which calls `keccak_absorb_blocks` directly, no feature +# needed); it is here so one flag means "accelerator on everywhere". The +# dependency is target-gated to riscv64 and cargo applies the forward only when +# the dependency is active, so host builds are unaffected — smoke-checked with +# `cargo check --features keccak-sponge-accel` on the host. +keccak-sponge-accel = ["lambda-vm-syscalls/keccak-sponge-accel"] + [dependencies] # Defines the `Crypto` trait, `CryptoError`, and `keccak::keccak_hash`. Same rev # + `default-features = false` as the guest's ethrex-crypto, so feature diff --git a/crypto/ethrex-crypto/src/lib.rs b/crypto/ethrex-crypto/src/lib.rs index ec36b0831..a0659bdd7 100644 --- a/crypto/ethrex-crypto/src/lib.rs +++ b/crypto/ethrex-crypto/src/lib.rs @@ -508,22 +508,42 @@ fn point_from_xy(x: &FieldElement, y: &FieldElement) -> Option { // ── Keccak-256 over the keccak_permute precompile (riscv64 guest) ─────────── -/// Keccak-256 sponge with an injected permutation function. +/// Keccak-256 sponge with injected primitives. /// /// Keccak-f[1600], rate 1088 bits (136 bytes), capacity 512 bits. /// Padding: `0x01 ... 0x80` (multi-rate, last bit set). The state is a /// 25-element u64 array; bytes are absorbed into the state via little-endian /// XOR (matching the standard Keccak byte-to-lane mapping). /// +/// `permute` runs one Keccak-f[1600]. `absorb_whole` is offered the message's +/// whole-rate-block prefix and returns how many of those blocks it absorbed +/// (XOR + permute each); returning 0 declines and leaves every block to the +/// software loop below. That is the seam the `ECALL -4` sponge accelerator +/// plugs into, and it is why the accelerator can bail out on an unmet +/// precondition without the caller knowing — both routes leave the same state. +/// +/// Padding never reaches `absorb_whole`: the final partial block is framed and +/// absorbed here, always through `permute`. +/// /// Gated to `riscv64 | test` so the generic function is available to the host /// unit tests without being dead code in the non-test host build. #[cfg(any(target_arch = "riscv64", test))] -fn keccak256_with_permute(input: &[u8], mut permute: F) -> [u8; 32] { +fn keccak256_with_backend(input: &[u8], mut permute: P, mut absorb_whole: A) -> [u8; 32] +where + P: FnMut(&mut [u64; 25]), + A: FnMut(&mut [u64; 25], &[u8]) -> usize, +{ const RATE: usize = 136; let mut state = [0u64; 25]; let mut offset = 0; + let whole_len = (input.len() / RATE) * RATE; + if whole_len > 0 { + offset = absorb_whole(&mut state, &input[..whole_len]) * RATE; + debug_assert!(offset <= whole_len); + } + while input.len() - offset >= RATE { absorb_block(&mut state, &input[offset..offset + RATE]); permute(&mut state); @@ -547,10 +567,63 @@ fn keccak256_with_permute(input: &[u8], mut permute: F output } -/// Keccak-256 via LambdaVM's `keccak_permute` syscall (riscv64 guest only). +/// Keccak-256 sponge driven by `permute` alone — the pure software absorb +/// path. Test-only: the guest goes through [`keccak256_with_backend`] so it can +/// offer the whole-block prefix to the accelerator. +#[cfg(test)] +fn keccak256_with_permute(input: &[u8], permute: F) -> [u8; 32] { + keccak256_with_backend(input, permute, |_, _| 0) +} + +/// Keccak-256 via LambdaVM's precompiles (riscv64 guest only): whole rate +/// blocks through the sponge-absorb accelerator when it is compiled in, the +/// padded tail always through `keccak_permute`. #[cfg(target_arch = "riscv64")] fn keccak256_via_lambdavm(input: &[u8]) -> [u8; 32] { - keccak256_with_permute(input, |s| lambda_vm_syscalls::syscalls::keccak_permute(s)) + keccak256_with_backend( + input, + |s| lambda_vm_syscalls::syscalls::keccak_permute(s), + absorb_whole_blocks_accel, + ) +} + +/// Whole-block absorb through the `KECCAK_SPONGE` accelerator (`ECALL -4`), +/// returning the number of blocks it took. +/// +/// The executor *traps* on an unmet precondition, so each one is either +/// discharged statically or checked here, and a failed check declines the whole +/// prefix (returns 0) rather than risking the run: +/// +/// - state 8-aligned: guaranteed, it is a `[u64; 25]`; +/// - data 8-aligned: checked — the guest heap (rlsf) hands out 16-aligned +/// payloads, but a node encoding borrowed at an odd offset would not be; +/// - `n_blocks > 0`: the caller only passes a non-empty whole-block prefix; +/// - low-limb room, i.e. `(addr mod 2^32) + last_offset < 2^32`: checked, since +/// the chip addresses each dword as `base_lo + offset` with no carry; +/// - regions disjoint: guaranteed, `state` is `&mut` and cannot alias `blocks`. +#[cfg(all(target_arch = "riscv64", feature = "keccak-sponge-accel"))] +fn absorb_whole_blocks_accel(state: &mut [u64; 25], blocks: &[u8]) -> usize { + const RATE: usize = 136; + const LOW_LIMB: u64 = 1 << 32; + + let low_limb_ok = + |addr: usize, len: usize| ((addr as u64) & (LOW_LIMB - 1)) + (len as u64 - 1) < LOW_LIMB; + if !(blocks.as_ptr() as usize).is_multiple_of(8) + || !low_limb_ok(blocks.as_ptr() as usize, blocks.len()) + || !low_limb_ok(state.as_ptr() as usize, 25 * 8) + { + return 0; + } + let n_blocks = blocks.len() / RATE; + lambda_vm_syscalls::syscalls::keccak_absorb_blocks(state, blocks, n_blocks); + n_blocks +} + +/// Accelerator compiled out: decline every block, so the sponge is exactly the +/// software one. +#[cfg(all(target_arch = "riscv64", not(feature = "keccak-sponge-accel")))] +fn absorb_whole_blocks_accel(_state: &mut [u64; 25], _blocks: &[u8]) -> usize { + 0 } /// XOR one rate-sized block of bytes into the state lanes (little-endian). diff --git a/crypto/ethrex-crypto/src/tests/keccak_tests.rs b/crypto/ethrex-crypto/src/tests/keccak_tests.rs index 14d497520..8beed458c 100644 --- a/crypto/ethrex-crypto/src/tests/keccak_tests.rs +++ b/crypto/ethrex-crypto/src/tests/keccak_tests.rs @@ -53,6 +53,71 @@ fn keccak_sponge_matches_trusted_permutation() { check_keccak(&[0xbb; 271]); } +/// Software mirror of the `ECALL -4` sponge-absorb accelerator, matching the +/// executor arm (`executor/src/vm/instruction/execution.rs`, +/// `SyscallNumbers::KeccakAbsorbBlocks`): per block, XOR 17 little-endian dword +/// lanes into the state, then permute. Lets the host test the *composition* the +/// guest uses — which blocks go to the chip, and where padding lands — without +/// a VM. +fn absorb_whole_blocks_mirror(state: &mut [u64; 25], blocks: &[u8]) -> usize { + const RATE: usize = 136; + assert_eq!(blocks.len() % RATE, 0); + let n_blocks = blocks.len() / RATE; + for k in 0..n_blocks { + absorb_block(state, &blocks[k * RATE..(k + 1) * RATE]); + keccak::f1600(state); + } + n_blocks +} + +/// The accelerated composition must be digest-identical to the software sponge +/// and to ethrex's reference `keccak_hash`, at every length that crosses a rate +/// boundary. This is the host half of the `keccak-sponge-accel` correctness +/// argument: it pins the *split* (whole blocks to the chip, padded tail to +/// `keccak_permute`), while the chip's own semantics are the executor's and the +/// prover's business. +/// +/// Also covers the accelerator DECLINING (returning 0, as it does on a +/// misaligned buffer): the software loop must then absorb everything and reach +/// the same digest. +#[test] +fn accelerated_absorb_matches_software_sponge() { + let data: Vec = (0..4 * 136 + 8).map(|i| (i * 97 + 13) as u8).collect(); + + for len in [ + 0, 1, 8, 135, 136, 137, 271, 272, 273, 407, 408, 409, 500, 544, 552, + ] { + let msg = &data[..len]; + let software = keccak256_with_permute(msg, keccak::f1600); + let accelerated = keccak256_with_backend(msg, keccak::f1600, absorb_whole_blocks_mirror); + let declined = keccak256_with_backend(msg, keccak::f1600, |_, _| 0); + + assert_eq!(accelerated, keccak_hash(msg), "vs reference, len={len}"); + assert_eq!(accelerated, software, "accel vs software, len={len}"); + assert_eq!(declined, software, "declined vs software, len={len}"); + } +} + +/// The seam lets the accelerator absorb only a PREFIX of the whole blocks it is +/// offered, with the software loop picking up the rest. Nothing in the guest +/// takes a partial bite today, but the contract allows it and an off-by-one in +/// the `offset` handoff would otherwise go unnoticed. +#[test] +fn partial_accelerated_take_matches_software_sponge() { + const RATE: usize = 136; + let data: Vec = (0..5 * RATE).map(|i| (i * 31 + 7) as u8).collect(); + + for len in [3 * RATE, 3 * RATE + 40, 5 * RATE] { + let msg = &data[..len]; + for take in 0..=len / RATE { + let got = keccak256_with_backend(msg, keccak::f1600, |state, blocks| { + absorb_whole_blocks_mirror(state, &blocks[..take * RATE]) + }); + assert_eq!(got, keccak_hash(msg), "len={len} take={take}"); + } + } +} + #[test] fn keccak_sponge_known_answer_vectors() { // Vectors from the Ethereum Yellow Paper / EIP-155. These use Keccak-256 diff --git a/executor/programs/rust/ethrex/Cargo.toml b/executor/programs/rust/ethrex/Cargo.toml index 4922712dd..97f74ce70 100644 --- a/executor/programs/rust/ethrex/Cargo.toml +++ b/executor/programs/rust/ethrex/Cargo.toml @@ -12,6 +12,33 @@ name = "ethrex" version = "0.1.0" edition = "2024" +[features] +# ON BY DEFAULT, deliberately. `/bench` builds the workload with a plain +# `make executor/program_artifacts/rust/ethrex.elf` and proves that one ELF, so +# the accelerator has to be in the default build or the bench cannot see it. +# `--no-default-features` still yields the plain software sponge — that is how +# `ethrex-nosponge.elf` is built for a local correctness A/B. +default = ["keccak-sponge-accel"] + +# Hash whole 136-byte keccak rate blocks on the KECCAK_SPONGE absorb +# accelerator (ECALL -4) rather than in guest software; the `10*1`-padded tail +# still goes through `keccak_permute`. The digests, and therefore the proven +# block, are identical either way. +# +# What this actually reaches: ethrex's trie node hashes, contract-code hashes, +# block/receipt hashes and the KECCAK256 opcode, all of which route through +# `Crypto::keccak256` -> `lambda-vm-ethrex-crypto`. It does NOT reach the +# `ethrex_crypto::keccak::keccak_hash` free function (software tiny-keccak), +# which on this ethrex rev is cold anyway — see ethrex-wiring.md §2. +# +# ⚠ An ELF built with this on runs `ECALL -4`, which only exists on an executor +# that has the KECCAK_SPONGE chip. It will NOT execute on `origin/main` until +# PR #912 lands — see the /bench fallback hazard in ethrex-wiring.md §10. +keccak-sponge-accel = [ + "lambda-vm-ethrex-crypto/keccak-sponge-accel", + "lambda-vm-syscalls/keccak-sponge-accel", +] + [dependencies] lambda-vm-syscalls = { path = "../../../../syscalls" } # LambdaVM crypto provider (keccak + ECSM-accelerated ecrecover), defined in the diff --git a/syscalls/Cargo.toml b/syscalls/Cargo.toml index 0460a2435..7861b679b 100644 --- a/syscalls/Cargo.toml +++ b/syscalls/Cargo.toml @@ -3,6 +3,14 @@ name = "lambda-vm-syscalls" version = "0.1.0" edition = "2024" +[features] +default = [] +# Route whole 136-byte keccak rate blocks through the KECCAK_SPONGE absorb +# accelerator (ECALL -4) instead of XOR-ing them into the state in guest +# software. Off by default: both variants stay buildable so the prover A/B is +# honest, and the digests are identical either way. +keccak-sponge-accel = [] + [dependencies] embedded-alloc = "0.6" riscv = { version = "0.15", features = ["critical-section-single-hart"] } diff --git a/syscalls/src/keccak.rs b/syscalls/src/keccak.rs index 9fe543c59..51c34d5b3 100644 --- a/syscalls/src/keccak.rs +++ b/syscalls/src/keccak.rs @@ -34,6 +34,37 @@ fn keccak_permute(state: &mut [u64; 25]) { keccak::f1600(state); } +#[cfg(all( + feature = "keccak-sponge-accel", + not(all(test, not(target_arch = "riscv64"))) +))] +use crate::syscalls::keccak_absorb_blocks; + +/// Software mirror of the `ECALL -4` sponge-absorb accelerator, so host +/// `cargo test --features keccak-sponge-accel` exercises the *composition* +/// (which blocks go to the accelerator, where padding lands) against the +/// reference digest. Semantics copied from the executor arm +/// (`executor/src/vm/instruction/execution.rs`, `SyscallNumbers::KeccakAbsorbBlocks`): +/// per block, XOR 17 little-endian dword lanes into the state, then permute. +/// +/// It counts the blocks it absorbs so the tests can assert the accelerated +/// path actually fired instead of passing vacuously. +#[cfg(all(feature = "keccak-sponge-accel", test, not(target_arch = "riscv64")))] +fn keccak_absorb_blocks(state: &mut [u64; 25], data: &[u8], n_blocks: usize) { + assert_eq!(data.len(), n_blocks * RATE_BYTES); + assert!(n_blocks > 0); + assert_eq!(data.as_ptr() as usize % 8, 0); + for k in 0..n_blocks { + let block = &data[k * RATE_BYTES..(k + 1) * RATE_BYTES]; + for (j, lane) in state.iter_mut().take(RATE_LANES).enumerate() { + let dword: &[u8; 8] = block[j * 8..j * 8 + 8].try_into().unwrap(); + *lane ^= u64::from_le_bytes(*dword); + } + keccak_permute(state); + } + tests::ABSORBED_BLOCKS.fetch_add(n_blocks, core::sync::atomic::Ordering::Relaxed); +} + /// Keccak-256 sponge rate in bytes (1088 bits = 136 bytes; capacity = 512 bits). const RATE_BYTES: usize = 136; @@ -49,6 +80,21 @@ const DELIMITER: u8 = 0x01; /// the two XORs combine to the single-byte `0x81` pad, per pad10*1. const FINAL_PAD_LANE_BIT: u64 = (0x80u64) << 56; +/// Guest-side mirror of the executor's `addr_limb_ok`: an +/// accelerator operand's LAST byte must fit inside the pointer's low 32-bit +/// limb, because the chip addresses each dword as `base_lo + offset` with no +/// carry into the high limb. The executor *traps* when this fails, so check it +/// here and fall back to software absorption instead — the fallback yields the +/// same digest, so this only ever costs cycles, never correctness. A 200-byte +/// state or a message buffer straddling a 4 GiB boundary is the only way to +/// hit it. +#[cfg(feature = "keccak-sponge-accel")] +#[inline(always)] +fn accel_low_limb_ok(addr: usize, len: usize) -> bool { + debug_assert!(len > 0); + ((addr as u64) & 0xFFFF_FFFF) + (len as u64 - 1) < (1u64 << 32) +} + /// Incremental Keccak-256 hasher; the state doubles as the absorption buffer. #[derive(Clone)] pub struct Keccak256 { @@ -92,6 +138,39 @@ impl Keccak256 { /// Absorb more input into the sponge. pub fn update(&mut self, mut input: &[u8]) { while !input.is_empty() { + // Sponge-absorb accelerator (ECALL -4): standing at a rate-block + // boundary with an 8-aligned pointer and at least one whole + // 136-byte block, hand ALL whole blocks to the chip in a single + // ecall. It XORs each block into lanes 0..17 and permutes, exactly + // what the two paths below do in guest software, so the sponge is + // left at `offset == 0` with `len % 136` bytes still to absorb — + // which the loop then feeds to the unchanged software path, and + // `finalize` pads as always. Padding never reaches the chip. + // + // Preconditions the executor enforces, and why each holds or is + // checked: 8-alignment of the state is guaranteed by `[u64; 25]`; + // 8-alignment of the data is the branch condition; `n_blocks > 0` + // follows from `len >= RATE_BYTES`; low-limb room is checked + // explicitly (see `accel_low_limb_ok`); and the state/data regions + // cannot overlap because `&mut self` is exclusive, so `input` + // cannot alias `self.state`. + #[cfg(feature = "keccak-sponge-accel")] + { + let n_blocks = input.len() / RATE_BYTES; + if cfg!(target_endian = "little") + && self.offset == 0 + && n_blocks > 0 + && (input.as_ptr() as usize).is_multiple_of(8) + && accel_low_limb_ok(input.as_ptr() as usize, n_blocks * RATE_BYTES) + && accel_low_limb_ok(self.state.as_ptr() as usize, 25 * 8) + { + let (blocks, rest) = input.split_at(n_blocks * RATE_BYTES); + keccak_absorb_blocks(&mut self.state, blocks, n_blocks); + input = rest; + continue; + } + } + // Whole-lane fast path: sponge offset on a lane boundary AND input // pointer 8-aligned (the VM traps on unaligned doubleword loads). // LE-only by construction: the raw `*const u64` read below equals the @@ -227,6 +306,68 @@ mod tests { RefKeccak256::digest(input).into() } + /// Whole rate blocks routed through the `ECALL -4` shim, process-wide. + /// Only meaningful as a "did the accelerated path fire at all" witness — + /// tests run in parallel, so compare against a snapshot with `>`, never `==`. + #[cfg(feature = "keccak-sponge-accel")] + pub(super) static ABSORBED_BLOCKS: core::sync::atomic::AtomicUsize = + core::sync::atomic::AtomicUsize::new(0); + + /// The A/B differential for the sponge-absorb accelerator. Run this file's + /// tests twice — with and without `--features keccak-sponge-accel` — and + /// both builds must match `sha3::Keccak256`; matching the same reference is + /// what makes the two guest variants digest-identical. + /// + /// The buffer is `repr(align(8))` so the accelerator's alignment + /// precondition is guaranteed rather than left to the allocator, and the + /// lengths straddle every interesting boundary: empty, sub-block, + /// rate−1/rate/rate+1, the same around 2 and 3 blocks, and ≥3-block + /// messages where the chip does real work. Each length is also fed as two + /// `update` calls so the accelerator is entered mid-stream (a split at 1 or + /// 8 leaves a non-zero sponge offset that the software path must drain + /// before the chip can take over). + #[test] + fn accel_length_sweep_matches_reference() { + #[repr(align(8))] + struct Aligned([u8; 640]); + + let mut buf = Aligned([0u8; 640]); + for (i, b) in buf.0.iter_mut().enumerate() { + *b = (i * 97 + 13) as u8; + } + assert_eq!(buf.0.as_ptr() as usize % 8, 0, "repr(align(8)) must hold"); + + #[cfg(feature = "keccak-sponge-accel")] + let absorbed_before = ABSORBED_BLOCKS.load(core::sync::atomic::Ordering::Relaxed); + + for len in [ + 0, 1, 8, 135, 136, 137, 271, 272, 273, 407, 408, 409, 500, 544, 640, + ] { + let msg = &buf.0[..len]; + assert_eq!(keccak256(msg), reference(msg), "one-shot len={len}"); + + for split in [1usize, 8, 64, 135, 136, 137] { + if split > len { + continue; + } + let mut hasher = Keccak256::new(); + hasher.update(&msg[..split]); + hasher.update(&msg[split..]); + let mut out = [0u8; 32]; + hasher.finalize(&mut out); + assert_eq!(out, reference(msg), "streaming len={len} split={split}"); + } + } + + // Without this the test would still pass if the accelerated branch were + // never taken (e.g. a mis-stated precondition silently disabling it). + #[cfg(feature = "keccak-sponge-accel")] + assert!( + ABSORBED_BLOCKS.load(core::sync::atomic::Ordering::Relaxed) > absorbed_before, + "accelerated absorb path never fired — the sweep proves nothing" + ); + } + /// Every length from empty through three full rate blocks (+2), so every /// padding boundary (135/136/137, 271/272/273, …) is hit. #[test]