feat(prover,executor): keccak sponge-absorb accelerator (ECALL -4, one row per rate block)

[MauroToscano]

What

A keccak sponge-absorb accelerator: new syscall keccak_absorb_blocks(state_ptr, data_ptr, n_blocks) at a7 = u64::MAX - 3 (spec ECALL -4; -3 is taken by the in-flight BLAKE3 PR #903), backed by a new KECCAK_SPONGE table with one row per absorbed 136-byte rate block. Per block k: state[0..17] ^= block_k (lanewise LE dwords), then keccak-f[1600] via the existing, untouched KECCAK_RND round chip. Lanes 17..25 pass through the XOR unchanged. Padding stays guest-side: the guest hashes the final 10*1-padded partial block through the classic per-permutation syscall, so the chip only ever sees whole rate blocks — no variable-length padding in-circuit.

Why: the guest-glue cost argument

Today the keccak accelerator does one permutation per ecall on a 200-byte in-place state, and the guest does the sponge in software: per 136-byte rate block it loads 17 message dwords, XORs them into the state and stores back — roughly 70–100 instructions of glue. In this VM a guest cycle costs on the order of ~250–300 committed cell-equivalents (CPU row + register MEMW rows + range-check/decode satellites + their aux columns), so that glue is ~15–25k cell-equivalents per permutation — a 20–35% tax on the ~73k-cell permutation itself, paid on every keccak256 in an ethrex block (trie nodes, tx hashes). PR #847 already attacked the same glue in guest software for the recursion verifier (−40% cycles); this PR moves the absorb into the chip.

What one KECCAK_SPONGE row costs instead: 690 main columns + ~108 aux columns (216 interactions) ≈ ~1k committed cells per block, replacing the ~15–25k of glue — the permutation's own 24 KECCAK_RND rows are unchanged. A loop of absorb calls costs ~7 guest cycles per call regardless of block count.

⚠ Block-level win pending flamegraph measurement of the sponge-glue share. The per-permutation arithmetic above is not a block-level claim: the EC-campaign lesson (PR #871) is to measure the target's share of total cells before claiming a workload win. A flamegraph of a real ethrex block quantifying the sponge-glue share should gate any headline number.

Soundness: per-block keying (the swap attack)

All n permutations of one absorb call share one CPU timestamp (the ecall is a single cycle). The Keccak bus tuple was (ts, round, state) and the round chip echoes ts. With two blocks at the same ts, a malicious prover could hand block A's permutation output to block B's row and vice versa — every tuple still appears exactly once per side, so the bus balances, and the chain equality between rows only forces some consistent assignment of outputs to rows, not the right one.

Fix (this PR):

• the Keccak bus payload gains a seq element: the classic core chip sends seq = 0, sponge row k sends seq = k, and KECCAK_RND carries seq through untouched like it carries ts (new SEQ column, 1480 → 1481 columns);
• the self-chain bus (KeccakSponge, BusId 32) is keyed (ts, seq) too: μ_first·SEQ = 0 anchors a call at SEQ = 0, the chain sender emits SEQ + 1, and a chain cannot wrap the field — so the permutations of one call carry distinct (ts, seq) keys on both Keccak-bus legs and the swap unbalances the bus;
• the chain also carries (n, state_ptr, block_base); the last row pins N_LO = SEQ + 1 and N_HI = 0 (word-level, which closes the N = n + p mod-p alias), so a call has exactly x12 rows; exactly-one-first-row and no-fork/no-merge fall out of the Ecall token and the memory argument.

The full attack walkthrough and the chain-shape argument are in the prover/src/tables/keccak_sponge.rs module docs. (This is the multi-permutation-per-ecall instance of DESIGN §7 item 10 from the BLAKE3 work.)

⚠ Wire-format break

The seq element changes the Keccak bus tuple for all proofs (the classic chip sends a constant 0), and KECCAK_RND gains a column: old proofs do not verify against this branch and vice versa. FIXED_TABLE_COUNT goes 10 → 11.

Always-on-AIR caveat / ABBA needed

KECCAK_SPONGE is an always-on table: every proof pays a near-empty AIR (min 4 rows × 690 main cols + ~108 aux cols) even when the workload never absorbs. This is the PR #871 regression shape (three near-empty always-on AIRs cost +25% prove time / +25% peak heap there). A /bench-abba run on a sponge-free workload (fib / ethrex) must gate the merge, plus a run on a keccak-heavy workload to measure the win. scripts/gen_keccak_absorb_bench.sh CALLS DATA_BLOCKS out.elf builds a sponge-saturated guest (each ecall absorbs DATA_BLOCKS blocks; CALLS-iteration loop), count-gated via the CLI's new KeccakAbsorb calls line.

Design deviations from the classic keccak chip

• Addressing uses the ECSM low-limb idiom, not keccak.rs's DWordHL pointer apparatus. Per-access addresses go on the Memw bus as base_lo + offset linear elements; the executor guarantees (base % 2^32) + last_offset < 2^32 for both regions (same guard as the ECSM operands). Fail-closed: a drifted base only produces Memw/Memory tokens with no matching PAGE/REGISTER cell. Rationale: the keccak apparatus costs 100 pointer columns + 100 IS_HALF sends per row — fine at one row per call, but it would roughly double this chip's per-block cost. state_ptr stays byte-decomposed (AreBytes + &7 alignment lookup) so alignment is enforced in-chip.
• State I/O is split: the first row does 25 pure lane reads at ts, the last row 25 write-only lane writes at ts + 1 (16-element Memw tuples; the MEMW table materializes old). A single combined read+write op per lane (keccak.rs style) is impossible here because no single row holds both the pre-call and the final state. The executor rejects state/data overlap so every (address, timestamp) pair stays unique.
• n_blocks is recovered from the x12 register state in the trace builder (the CPU log's two free slots carry the state/data addresses), like the ECSM operand addresses.

Executor guards

Both pointers 8-aligned; n_blocks > 0; the LAST byte of each region checked against u64 overflow (checked_mul/checked_add) and low-limb overflow; state/data regions disjoint (an overlap would put two MEMW ops on one (address, timestamp) pair, which the memory argument cannot order — same rationale as EcsmOperandOverlap).

Tests

• executor: sponge differential vs tiny_keccak (n = 1, 2, 3, 5, 8, 13, seeded pseudo-random state+data), a chained XOR+keccak_f1600 replay, one rejection test per guard incl. both sides of the low-limb boundary — 12/12;
• chip: constraint-set exactly-once/degree/folder-capture agreement (check_table), program + device interpreter differentials, and a full sender ↔ collector multiset equality (chip + KECCAK_RND ByteAlu/AreBytes sends evaluated off the generated traces vs collect_bitwise_from_keccak_sponge, over a 3-block call plus an n = 1 call) + a no-IS_HALF guard;
• e2e: test_prove_elfs_keccak_absorb — asm guest absorbs 3 blocks in one ecall, committed state cross-checked against a tiny-keccak sponge replay, then full prove + verify;
• full prove_elfs_tests suite green (102 passed); make lint clippy passes (×4 feature combos) clean.

Not in this PR

• Guest-side switch of real hashing code paths (ethrex / recursion verifier) onto the new syscall.
• Benches (see the ABBA note above).
• GPU box validation for the new table (the IR device-lowering differential is covered by constraint_program_device_tests; box validation pending).