spec: fix keccak's addr handling

[erik-3milabs]

No description provided.

[github-actions]

Codex Code Review

No issues found in the PR diff.

The changes are limited to Keccak spec metadata/constraints and documentation. The new addr/state_ptr half-limb range checks are consistent with the existing MEMW register-read and ADD template patterns used elsewhere. git diff --check is clean.

[claude]

Review: spec: fix keccak's addr handling

Overall: Correct and well-targeted fix. The three changes are coherent and address a real gap in the constraint system.

What this does

1. Type fix — addr changed from DWordBL (byte-limbed, 8 elements) to DWordHL (half-limbed, 4 elements), aligning it with state_ptr which already uses [["DWordHL", 5], 5]. DWordBL would have required IS_BYTE range checks; DWordHL uses IS_HALF, consistent with the RISC-V address representation used elsewhere.

2. New range_addr constraint — IS_HALF × 4 limbs. This is necessary: IS_HALF on the 4 half-limbs of addr implies IS_WORD on the 2 word-limbs when cast to DWordWL, satisfying the ADD chip's @add:a:lhs assumption for the state_ptr derivation at @keccak:c:state_ptr.

3. MEMW fix — With DWordHL (4 limbs), addr can no longer be passed directly as the 8-element MEMW value array. Explicitly constructing ["arr", WL[0], WL[1], 0, 0, 0, 0, 0, 0] (the 2 meaningful word-limbs + 6 zeros) is the correct solution given write2=1.

4. Added ref on the existing range_state_ptr IS_HALF constraint — minor but needed for the new cross-reference in the .typ text.

One documentation gap

The updated prose in keccak.typ explains that @keccak:c:range_state_ptr satisfies @add:a:sum, but the analogous purpose of the new @keccak:c:range_addr (satisfying @add:a:lhs) goes unmentioned. A reader will see the new constraint without knowing why it exists. Worth adding a note like: @keccak:c:range_addr is included to satisfy @add:a:lhs.

No correctness issues found.

[claude]

The text explains that @keccak:c:range_state_ptr satisfies @add:a:sum, but the new @keccak:c:range_addr constraint's purpose (satisfying @add:a:lhs for the ADD chip used in @keccak:c:state_ptr) isn't mentioned. Consider adding something like: @keccak:c:range_addr is included to satisfy @add:a:lhs.

[RobinJadoul]

I think technically we can do a DWordWL here?
We're not using addr anywhere else other than computing state_ptr, so we can get WL range check from the memory and not need the IS_HALF checks.
This does imply a change to the first bullet point in "Notes/potential optimizations" too.

[erik-3milabs]

I mean, while we're at it, we might as well drop addrand just load the first address in state_ptr[0][0]? That would still leave the optimization that state_ptr[0][0] could be a DWordWL (while the others have to be HLs), which I think we should forego in favor of a more readable spec. Wdyt?

[RobinJadoul]

Sure.
I think the only reason we didn't do that in the first place was to keep the range_ptr ADD iter clean, but we can even keep it as-is, given that ADD<x; x, 0> works just fine