Spec: COPY accelerator

[nicole-graus]

Description

Specifies the accelerator implemented in #984.

• New MEMMOVE chapter covering memcpy, memmove, memset and commit. The destination domain and the read/write timestamp order are decoded from the entry point, never chosen by the caller: is_set from the syscall number, is_commit from which bus the first row accepted from, both carried inside MEMMOVE_NEXT so a sequence cannot change functionality midway.
• COMMIT is now one row per ecall: it keeps the syscall number and the x254 update, and defers the byte loop over COMMIT_DEFER. CNB is retired.
• Adds the ADDNW template, which is what rules out a sequence closing into a ring.
• Allocates ECALL -30 (copy) and -32 (memset), and lists -31 as reserved for HINT so it is not handed out twice.

[github-actions]

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

---

Automated review by Kimi (Moonshot AI)

[github-actions]

Codex Code Review

• Medium — Commitment indexing becomes inconsistent above 4 GiB. In memmove.toml:350, ADDNW normalizes dst_incr into two 32-bit limbs, but COMMIT and the existing commitment-domain convention represent indices as [index, 0]. After crossing 2^32, subsequent rows emit addresses such as [8, 1] instead of [2^32 + 8, 0]. These are different memory tuples, so otherwise valid commitments cannot balance against the verifier’s output. Preserve scalar indexing for commitments, or update the producer and verifier to use normalized indices consistently.

[github-actions]

Kimi Code Review

⚠️ Review failed: Kimi API request failed with status 401

---

Automated review by Kimi (Moonshot AI)

[github-actions]

Codex Code Review

• Medium — Commitment indices change representation after 4 GiB (memmove.toml). dst_incr normalizes the commitment index into two 32-bit limbs, while COMMIT and the verifier use [index, 0]. A write spanning index 2^32 therefore emits [0, 1] where the verifier expects [2^32, 0], making valid output unprovable. Preserve the existing field-valued index arithmetic for commitments, or update the producer and verifier to use the same normalized representation.

[erik-3milabs]

First set of comments. Primary change request: the COMMIT chip should be completely integrated into the MEMMOVE chip; no COMMIT chip should be needed after this PR is done.

Once this is done, I'd be happy to give this another review!

[RobinJadoul]

/ai-review

[github-actions]

AI Review

PR #986 · 7 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[github-actions]

Codex Code Review

• Low — Duplicate IS_WHH signature (spec/src/signatures.toml:167): This signature already exists at line 186. The signatures chapter renders both entries and counts the same template twice. Remove the added duplicate.

No other concrete safety, correctness, or significant performance issues found in the PR diff. Review was static; no builds or tests were run.

[claude]

Review summary (static review of the spec diff)

Critical

• memset uses ECALL -31, which is already HINT's number (hint.rs: u64::MAX - 30). Two receivers on the same ECALL number let the prover choose which chip balances the CPU's send. The PR description says memset is -32 and -31 is reserved for HINT, but the code doesn't match. See the inline comment.

High

• write_value passes 2*is_write into MEMW, whose first input is typed is_register: Bit.
• The explanation of how domain 2 (committed output) is initialized and finalized by the verifier, and of the verifier's check on x254, was removed along with commit.typ and wasn't carried over.

PR description out of date

• It describes a MEMMOVE chapter, is_commit, COMMIT_DEFER, an ADDNW template and a kept one-row COMMIT chip. None of these are in this diff, which instead adds a single COPY chip, deletes COMMIT and uses prover-hinted is_set/is_write. Please update the description, or push the missing commits.

Checked and looks correct

• Termination logic: end exactly when count = step or a zero-length first row.
• Memmove overlap: all reads at t, all writes at t+1, so overlapping ranges still see the original source bytes.
• Memset: the reversed read/write order together with the dst = src + 8 gap repeats the first 8 bytes.
• Padding rows: they satisfy the unconditioned ADD constraints.
• Flag carry-over: is_set and is_write are passed through COPY_NEXT, so a sequence can't switch mode midway.

Minor

• dst_res_is_write and range_dst_res could use first_write instead of is_write as their condition, since dst_res is only consumed on first rows.