Keccak spec mismatches affecting verification

[jotabulacios]

While implementing the Keccak precompile #519 , we found two spec-level mismatches that break end-to-end verification.

Mismatch 1 - Off-by-one carry offset in rotated_Cxz and rho

Files / lines

• spec/src/keccak_round.toml:78 — rotated_Cxz virtual
• spec/src/keccak_round.toml:102, 110, 118, 126 — four rho mux cases

Root cause

HWSL(hw, z) produces a 16-bit carry (SLLC), which occupies 2 bytes in Cxz_right. The spec formulas propagate that carry with a 1-byte shift (z-1, z-3, z-5, z-7). It should be a 2-byte shift.

Byte-level proof

Take Cxz = 0x8000_0000_0000_0000, rotate left by 1, expected 0x0000_0000_0000_0001.

After HWSL per halfword: Cxz_right = [0, 0, 0, 0, 0, 0, 0x01, 0x00] (SLLC₃ at bytes 6–7).

At z=0, the target output byte is 0x01.

• Spec: Cxz_right[(0-1) mod 8] = Cxz_right[7] = 0x00 (bit dropped)
• Correct: Cxz_right[(0-2) mod 8] = Cxz_right[6] = 0x01

Empirical failures (applying spec literally):

• test_keccak_round_trace_matches_f1600 diverges from keccak_f1600 at round 2, lane (0,0), byte 6 (expected 32, got 48).
• test_keccak_core_round_state_consistency wrong at round 23.
• test_prove_elfs_keccak — STARK verifier rejects the proof.

Proposed fix — spec/src/keccak_round.toml:

Line	Current	Fix
78 (rotated_Cxz)	["-", "z", 1]	["-", "z", 2]
102 (rho case 0)	["-", "z", 1]	["-", "z", 2]
110 (rho case 1)	["-", "z", 3]	["-", "z", 4]
118 (rho case 2)	["-", "z", 5]	["-", "z", 6]
126 (rho case 3)	["-", "z", 7]	["-", "z", 8] (or ["mod", "z", 8])

Mismatch 2 - ECALL payload field-ordering mismatch

File / line

• spec/src/keccak.toml:51

Root cause

The keccak ECALL payload uses arr(hi32, lo32). Every other ECALL receiver (halt.toml, commit.toml) and every other arr(...) in the spec uses [lo, hi] per the DWordWL convention (config.toml:69-74). The shared CPU sender also emits [lo, hi]. Because LogUp fingerprints are order-sensitive, the bus doesn't balance.

Current

input = ["timestamp", ["arr", ["-", ["^", 2, 32], 1], ["-", ["^", 2, 32], 2]]]
# flattens to [ts_lo, ts_hi, 2^32-1, 2^32-2] = [ts_lo, ts_hi, hi32_of_-2, lo32_of_-2]

Comparison

Chip	Spec	Flattened	Matches CPU sender [ts_lo, ts_hi, lo, hi]?
HALT	cast(93, DWordWL)	[ts_lo, ts_hi, 93, 0]	✓
COMMIT	cast(64, DWordWL)	[ts_lo, ts_hi, 64, 0]	✓
KECCAK	arr(2^32-1, 2^32-2)	[ts_lo, ts_hi, hi, lo]	✗

Empirical failure

Applying the spec literally (receiver in [hi, lo] order while CPU sends [lo, hi]): test_prove_elfs_keccak fails with LogUp bus does not balance.

Proposed fix — spec/src/keccak.toml:51:

# Before
input = ["timestamp", ["arr", ["-", ["^", 2, 32], 1], ["-", ["^", 2, 32], 2]]]

# After
input = ["timestamp", ["cast", -2, "DWordWL"]]

cast(-2, DWordWL) produces [lo32, hi32] = [2^32-2, 2^32-1], matching the CPU sender and HALT/COMMIT.

[jotabulacios]

Verified the fix and it's working perfectly, thanks!