Update spec

[ColoCarletti]

No description provided.

[github-actions]

Codex Code Review

Found two issues in the PR diff:

1. [High] SHA-256 ROTXOR leaves upper half unconstrained
   In spec/src/rotxor.toml:157, the second a2 limb constraint is documented as constraining a2[1], but the polynomial subtracts a2[0] again. This means a2[1] is not tied to the shifted/rotated input, so the upper 16 bits of the third ROTXOR term can be chosen arbitrarily and then flow into SHA-256 round/message-schedule values. Change the first indexed limb in that polynomial from 0 to 1.

2. [High] SHA-256 x11 read emits the wrong old register value
   In spec/src/sha256.toml:59, the MEMW output for reading m_addr from x11 uses limb 0 twice. It should mirror the input value’s low and high limbs, like the h_addr read below does. As written, the accelerator consumes an old x11 token [lo, lo] and emits [lo, hi], so the “read” mutates the register and rejects normal cases where hi != lo.

I also ran the spec typechecker command:

python3 spec/tooling/chip.py spec/src/config.toml spec/src/signatures.toml spec/src/*.toml

It reports no issues, so these are semantic bugs the current checker does not catch.

[claude]

Review: Update spec (SHA256 + KECCAK accelerators)

Summary

This PR adds formal specification for two cryptographic accelerators (SHA256 and KECCAK permutation), introduces the IS_BYTE template (wrapping the renamed ARE_BYTES interaction), extends the expression language with mod, and supports nested array types. The bulk of the new material is correct and well-structured.

Bugs

1. [High] rotxor.toml — a2[1] constraint uses wrong index (see inline)

The polynomial for the second a2 constraint has ["idx", ["cast", "a2", "WordHL"], 0] where it should be 1. This means a2[0] is constrained twice and a2[1] is unconstrained — a prover can freely set it, breaking the shift decomposition for SHA256's s0/s1 computations.

2. [Medium] sha256.toml — m_addr MEMW output duplicates index 0 (see inline)

The MEMW output for reading register x11 (chunk address) uses ["idx", ..., 0] twice instead of 0 then 1. The high word of m_addr[0] is left unconstrained; the analogous h_addr read on line 106 is correct.

Nit

• signatures.toml line 8: comment says IS_BIT<X, μ> — should be IS_BYTE<X, μ> (copy-paste from the entry above).

No issues found in

• Keccak theta/rho/chi/iota constraint structure (range checks on Cxz_left, rot_left, rot_right are correctly noted as necessary and present)
• mod expression addition in expr.typ / chip.py
• IS_BYTE → template + ARE_BYTES interaction split
• Nested array type support
• CPU pc_double_read / prev_pc_timestamp_borrow inline optimization
• Build script (build_shiroa.sh)