perf(keccak): inline θ/ρ halfword shifts as μ-gated identities, drop 120 HWSL sends/row

[MauroToscano]

What

Replace the 120 HWSL bus sends per KECCAK_RND row (θ rotate-by-1: 20, ρ shifts: 100) with μ-gated degree-2 linear identities over the same committed cells:

in · 2^rnc = right · 2^16 + left

The existing IS_BYTE and IS_BIT checks make the split unique: given left, right ∈ [0, 2^16), the pair is the Euclidean quotient/remainder of in · 2^rnc ÷ 2^16 (all values < 2^32 ≪ p, so field semantics = integer semantics). A shift by a compile-time constant is field-linear, so the lookup bought nothing the identity doesn't — it only paid LogUp aux.

• Sends/row: 1151 → 1031 (HWSL → 0) ⇒ −60 aux extension columns = −180 committed base cells/row (~4.3k/permutation), zero new columns
• Constraints: 20 → 140, all degree ≤ 3 (max_degree() unchanged)
• Not wire-identical (aux layout shrinks) — old proofs verify with old verifier, new with new

Spec

This matches the chip spec as updated by the research team on spec/main (d397668, #873), which replaces the θ/ρ HWSL interactions with the same arith identities. This PR intentionally carries only the Rust code; main's copy of spec/src/keccak_round.toml still shows the HWSL form and needs the tooling const-propagation from #873 to typecheck the new one, so syncing it is left to the spec-sync flow.

Supersedes #860, which carried the same code plus an alternative spec toml and the z3 verification evidence; see there for the formal-equivalence gate and the full A/B.

Bench

From #860, pure-keccak guest (5000 keccak-f syscalls, single-epoch continuation proof), 32-core box, alternated A/B ×4: −6.8% median prover time (13.982s → 13.027s, distributions disjoint, cv ≈ 1.3%). keccak_rnd was 86.6% of committed cells in that bench; the measured committed-cell delta matched the predicted −180 cells/row. Measured before the transcript rewrite (#841) landed, so worth a fresh /bench here before merge.

Tests

• test_keccak_constraint_counts (140), test_keccak_bitwise_ops_count (HWSL 2880 → 0), test_keccak_bus_interaction_counts, test_keccak_column_counts
• keccak_rnd_constraint_set_folder_capture_agree (prover folder ≡ verifier folder ≡ captured IR)
• e2e: test_prove_elfs_keccak, _keccak_multi_call (tiny-keccak cross-check), _unaligned_state_addr (tamper still rejected)
• make lint clean

[MauroToscano]

/bench

[MauroToscano]

/bench-gpu

[github-actions]

GPU Benchmark (ABBA) — c0f259cbae vs main (8 pairs)

_{RTX 5090 · Vast.ai datacenter @ $0.6685185185185185/hr · prover/cuda · ethrex real block, continuations · drift-free A/B/B/A}

❌ Run failed. Last log lines:

[MauroToscano]

/bench-gpu

[github-actions]

Benchmark — real block (ethrex_mainnet_25368371.bin) (median of 5)

_{continuations · epoch 2^22 · 13 epochs}

Metric	main	PR	Δ
Peak heap	52097 MB	51975 MB	-122 MB (-0.2%) ⚪
Prove time	159.529s	158.298s	-1.231s (-0.8%) ⚪

✅ No significant change.

_{Prove-time spread 1.9% (156.677s / 159.747s / 158.543s / 157.769s / 158.298s)}

_{Commit: 6b538c6 · Baseline: cached · Runner: self-hosted bench}

[MauroToscano]

/bench

[MauroToscano]

/bench-gpu

[MauroToscano]

/bench 5

[MauroToscano]

/bench-gpu 8

[MauroToscano]

/bench-gpu 8