feat(prover): Add Keccak precompile

[jotabulacios]

This PR adds the Keccak precompile. The permutation is implemented in the executor (keccak_f1600, verified against tiny-keccak) and proven by three chips:

1. KECCAK core (511 columns): ECALL receiver, one row per call, issues 25 combined MEMW read+write ops for the 200-byte state, packs the state into Word4L halves, and sends to the Keccak round bus.
2. KECCAK_RND round chip (1,480 columns, 24 rows per call): runs one round per row. Theta / rho / pi / chi / iota are enforced through a mix of BITWISE lookups (XOR_BYTE, AND_BYTE, HWSL, IS_BYTE) and polynomial constraints (IS_BIT on the round-constant / rho-case selector bits, rnc equality, and the degree-3 pi mux).
3. KECCAK_RC table (10 columns, preprocessed, 24 rows padded to 32): supplies the round constants via 1 bus interaction

[erik-3milabs]

FYI: the spec is merged (#474) GL!

[github-actions]

Benchmark Results for modified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head keccak	103.5 ± 3.0	97.7	107.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head syscall_commit	77.3 ± 1.1	75.9	78.7	1.00

[github-actions]

Codex Code Review

• High: The Keccak proof path accepts unaligned state pointers even though execution rejects them. The executor performs load_doubleword/store_doubleword, which return UnalignedAccess unless x10 is 8-byte aligned (execution.rs, memory.rs). The prover reconstructs the state byte-by-byte and routes it through the generic unaligned MEMW path (trace_builder.rs, trace_builder.rs, memw.rs), while the new Keccak AIR only enforces state_ptr = addr + 8*i (keccak.rs). That is a VM/proof mismatch: a malicious prover can prove a Keccak syscall the VM would have trapped on. Add an explicit 8-byte alignment check for state_addr, or route these accesses through an aligned-only memory path.

• High: Address overflow semantics diverge between executor and prover. Execution uses plain state_addr + i*8 and then address + 4 inside the doubleword helpers (execution.rs, memory.rs), but the prover uses wrapping_add when collecting Keccak ops and when materializing state_ptr (trace_builder.rs, trace_builder.rs, keccak.rs). Near u64::MAX, the proof system will wrap accesses back to low memory, while the executor will panic in debug or hit different addresses. Reject overflowing state ranges up front and use checked arithmetic on both sides.

I couldn’t run the targeted tests here because cargo/rustup failed to create temp files under the read-only /home/runner/.rustup path.

[claude]

Review: Keccak-f[1600] precompile

The implementation is solid — the permutation arithmetic, rho/pi/chi bus wiring, and test coverage all look correct. A few issues to address before merging:

Medium

• Overflow in executor (×2): state_addr + (i as u64) * 8 uses unchecked arithmetic; panics in debug on near-u64::MAX addresses, silently wraps in release. The trace builder already uses wrapping_add — the executor should too.
• Dead bus ID: BusId::EcallKeccak (ID 22) is defined but no chip sends or receives on it. The keccak core uses the shared BusId::Ecall. Either remove it or document the intent.

Low

• Duplicate round constants: keccak_rc.rs defines its own private RC: [u64; 24] instead of importing KECCAK_RC from execution.rs (which keccak_rnd.rs already does). Silent divergence risk.
• Misleading enum discriminant: KeccakPermute = 94 looks like a real syscall number. Casting it to u64 gives 94, not u64::MAX - 1. Worth a compile-time assert or a _placeholder suffix to make the intent unmistakable.
• Inconsistent chi indexing: chi(x,y) = x*5+y while every other state-array helper uses x+5*y. Cosmetic but easily trips a reader comparing chi_ands with chi side-by-side.

[github-actions]

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base binary_search	68.2 ± 12.0	58.0	86.0	1.14 ± 0.20
head binary_search	59.8 ± 0.5	59.1	60.8	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	59.3 ± 1.5	58.2	61.6	1.00
head bitwise_ops	59.9 ± 1.0	58.6	61.0	1.01 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	63.7 ± 1.0	63.0	66.2	1.00
head fibonacci_26	64.6 ± 1.2	63.0	65.7	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base hashmap	137.5 ± 4.0	130.9	141.9	1.00
head hashmap	139.1 ± 4.2	134.4	148.3	1.01 ± 0.04

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	63.5 ± 0.9	62.0	64.7	1.00
head matrix_multiply	64.4 ± 1.2	62.6	66.6	1.02 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	59.6 ± 0.7	58.7	60.5	1.00
head modular_exp	63.4 ± 7.2	59.5	78.0	1.06 ± 0.12

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	62.6 ± 0.6	61.8	63.6	1.00
head quicksort	63.5 ± 0.9	62.3	64.6	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	64.9 ± 0.4	64.4	65.5	1.00
head sieve	66.0 ± 1.2	64.7	67.6	1.02 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	73.7 ± 0.6	72.8	74.8	1.00
head sum_array	76.3 ± 4.4	73.4	88.4	1.04 ± 0.06