diff --git a/spec/chapters/about_ecalls.typ b/spec/chapters/about_ecalls.typ
index 102d7a504..e2f6e0b2c 100644
--- a/spec/chapters/about_ecalls.typ
+++ b/spec/chapters/about_ecalls.typ
@@ -35,3 +35,6 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our
 / -20: `FEXT_LOAD` (@fext)
 / -21: `FEXT_FMA` (@fext)
 / -22: `FEXT_ZERO` (@fext)
+/ -30: `MEMMOVE`/`memcpy`/`memmove` (@memmove)
+/ -31: `HINT` (reserved, not yet specified)
+/ -32: `MEMMOVE`/`memset` (@memmove)
diff --git a/spec/chapters/add.typ b/spec/chapters/add.typ
index a3e64f493..0c1288c03 100644
--- a/spec/chapters/add.typ
+++ b/spec/chapters/add.typ
@@ -5,12 +5,15 @@
 #let config = load_config()
 #let chip = load_chip("src/add.toml", config)
 #let subchip = load_chip("src/sub.toml", config)
+#let nwchip = load_chip("src/add_nw.toml", config)
 
 #set_nr_interactions(chip, name: "SUB")
 #let nr_interactions = compute_nr_interactions(chip)
+#let nw_interactions = compute_nr_interactions(nwchip)
 
 #let add = raw(chip.name)
 #let sub = raw(subchip.name)
+#let addnw = raw(nwchip.name)
 
 = #add
 #add is a constraint template that is used to assert that $#`sum` equiv #`lhs` + #`rhs` (mod 2^64)$, under the condition that `cond` is non-zero.
@@ -50,3 +53,27 @@ This template introduces #nr_interactions interaction(s).
 == Constraints
 This template introduces the following constraints
 #render_constraint_table(subchip, config)
+
+= #addnw
+
+#add asserts an equality modulo $2^64$; #addnw is the variant that rules out the wraparound.
+It constrains that $#`sum` = #`lhs` + #`rhs`$ _over the integers_ when the expression `cond` is non-zero, and is intended for chips whose operands are addresses, where a wraparound would silently move an access to an unrelated region of memory.
+
+== Variables
+This template introduces #nw_interactions interaction(s).
+#render_chip_variable_table(nwchip, config)
+
+== Assumptions
+#render_chip_assumptions(nwchip, config)
+
+== Constraints
+This template introduces the following constraints
+#render_constraint_table(nwchip, config)
+
+Note that `carry` is defined exactly as it is in #add, so @addnw:c:no_wraparound is precisely the statement that the addition of the most significant limbs does not carry out;
+combined with @addnw:a:sum, that is equivalent to $#`lhs` + #`rhs` < 2^64$.
+
+The two limbs are treated asymmetrically, and deliberately so.
+The carry out of the _least_ significant limb is constrained on every row, so the low limb of `sum` always means what it says.
+The carry out of the _most_ significant limb is pinned only where `cond` is non-zero, which leaves `sum`'s high limb free on the rows where a chip does not consume the result --- typically padding rows, and the terminal row of a recursive sequence.
+Constraining it there would buy nothing and would force those rows to carry a well-formed successor they never use.
diff --git a/spec/chapters/commit.typ b/spec/chapters/commit.typ
index 14aa1dedc..ffe7230ef 100644
--- a/spec/chapters/commit.typ
+++ b/spec/chapters/commit.typ
@@ -1,4 +1,3 @@
-#import "/meta.typ": aside
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_variable_table,
@@ -6,7 +5,6 @@
   total_nr_instantiated_columns,
   compute_nr_interactions,
   render_constraint_table,
-  render_chip_assumptions,
   render_chip_padding_table,
 )
 
@@ -14,22 +12,21 @@
 #let chip = load_chip("src/commit.toml", config)
 #let commit = raw(chip.name)
 
+The #commit chip handles the `write` system call: it accepts the call, checks the file descriptor, advances the commitment index and hands the bytes themselves to `MEMMOVE` (@memmove).
+It is one row per system call; the loop over the buffer lives in the other chip.
+
 = Variables
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 #let nr_interactions = compute_nr_interactions(chip)
 
-The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions:
+The #commit chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
 #render_chip_variable_table(chip, config)
 
 = Constraints
 In this VM, committing is considered equivalent to writing a value to `stdout`.
 Hence, this chip responds to `ECALL`s with system call number 64.
 #footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L174")[[src]]])
-Since we do not know how many bytes are to be committed, this chip employs a recursive design:
-each iteration commits one byte, and recursively "calls" itself to commit the remaining bytes.
-As such, only the call from the CPU to this chip (i.e., the `first` in the recursion tree) should accept the `ECALL`; later recursive calls should not.
-This is why @commit:c:receive_ecall has multiplicity $-#`first`$.
 #render_constraint_table(chip, config, groups: "incoming")
 
 The `write` operation --- writing to a file descriptor --- has the following signature:
@@ -41,7 +38,7 @@ ssize_t write(size_t count; int fd, const void buf[count], size_t count);
 
 That is to say,
 - `A0` contains the file descriptor,
-- `A1` contains the address of `buf`'s first byte, 
+- `A1` contains the address of `buf`'s first byte,
 - `A2` contains `count`, and
 - the written count should be written to `A0`.
 
@@ -49,76 +46,35 @@ That is to say,
 Since we only support writing to `stdout` (which corresponds to $#`fd` = 1$
 #footnote([The Open Group Standard for Information Technology --- Portable Operating System Interface (POSIX) Base Specifications, `unistd.h`; The Open Group, issue 8, #link("https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/unistd.h.html")[[src]]]))
 we assert that `x10` contains $1$ in @commit:c:read_fd_write_count.
-Note that this constraint _also_ writes `count` to `A0`; 
+Note that this constraint _also_ writes `count` to `A0`;
 in this VM it is impossible for a commit to be interrupted or fail.
 Lastly, the `index` is read from `x254`#footnote([In this VM, register 254 is reserved for containing the commitment index.]); in the same operation, $#`index` + #`count`$ is written back to this location by @commit:c:read_index.
-This, too, leverages the fact that a commit will not be interrupted or fail to update the `index` for the next commit sequence.
-Again, each of these memory interactions only take place when this is the `first` call in the recursion tree.
-
+This, too, leverages the fact that a commit will not be interrupted or fail to update the `index` for the next commitment sequence.
 #render_constraint_table(chip, config, groups: "read_input")
 
-*Note*: the observant reader will notice that @commit:c:read_index casts `count` to a `BaseField`, potentiallly losing information.
+*Note*: the observant reader will notice that @commit:c:read_index casts `count` to a `BaseField`, potentially losing information.
 This is indeed correct.
 However, since it is practically impossible to commit more than $2^64-2^32$ bytes in a single VM execution, it was decided to permit this.
 
-Next, we read the `value` located at buffer address `address` and commit to it under the given `index`.
-This is only performed when we have not yet reached the `end` of the commit sequence.
-Values are committed by letting the verifier initialize and finalize the global memory argument (see @memory and @streaming),
-with the claimed commitments in its own domain separated part of memory, with domain separator value 2.#footnote[
-  In order to make sure the verifier can properly finalize the committed values, the last epoch can "bring forward"
-  all commitments from earlier epochs, similar to padded values, in the `L2G` table.
-  Then the contribution of the commitments only consists of the tuples `(2, address, last_epoch_index, value)`, which is entirely known to the verifier.
-]
-This chip then checks that the same value as the one being committed is then found at the corresponding address.
-In doing this, we enforce that all values being committed match the claimed commitment,
-and the verifier should additionally check that register 254 contains the correct value to ensure
-the correct amount of bytes have been committed.#footnote[
-  We additionally note here that for very large commitments (with index $>= 2^32$),
-  the (commit space) address can potentially become denormalized, but since no other chips or systems interact with
-  this memory domain, there is no issue.
-  The usual consistency guarantee from the LogUp argument and correct initialization as for general addresses applies.
-]
-#render_constraint_table(chip, config, groups: "commit")
-
-In parallel, we compute $#`address_incr` = #`address` + 1$ (@commit:c:address_incr) as address of the next byte to commit, and $#`count_decr` = #`count` - 1$ (@commit:c:count_decr) as the number of bytes that still has to be committed after committing this byte.
-@commit:c:range_address_incr and @commit:c:range_count_decr are included to satisfy @add:a:sum respectively @sub:a:diff.
-#render_constraint_table(chip, config, groups: "incr_decr")
-
-When `count` hits $0$, we should stop performing further recursive calls.
-We use the `end` bit to indicate these circumstances.
-
-#render_constraint_table(chip, config, groups: "end")
-
-*Note*: 
-+ Rather than setting $#`end` = 1$ when $#`count` = 0$, we do so when $#`count_decr` = -1$.
-  This technique allows `count` to be stored in a `DWordWL` rather than a `DWordHL`, saving two columns.
-+ $forall i in [0, 3]: 65535 - #`count_decr`_i >= 0$ as a result of @commit:c:range_count_decr.
- Hence, 
-  $
-  sum_(i=0)^3 65535 - #`count_decr`_i = 0 arrow.l.r.double.long forall i in [0, 3]: #`count_decr`_i = 65535
-  $
-
-When this was not the `end` byte to commit in this recursion sequence, we recursively _Commit the Next Byte_ (`CNB`), specifying the timestamp, address to continue reading and the number of bytes that should still be committed (@commit:c:send_commit_next_byte).
-Since that certainly won't be the `first` call in the sequence, we read `address_incr` and `count_decr` from the previous recursion level into `address` and `count` and continue executing the commit.
-#render_constraint_table(chip, config, groups: "lookups")
-
-Lastly, we must make sure `first`, `end` and `μ` are bits (@commit:c:range_first, @commit:c:range_end, @commit:c:range_mu), and that when either $#`first` = 1$ or $#`end` = 1$ imply that $#`μ` = 1$ (@commit:c:first_or_end_implies_mu).
-These are required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary.
+The bytes themselves are copied by `MEMMOVE`, from `address` in RAM to the commitment domain starting at `index`.
+@commit:c:defer_to_memmove is the whole of that hand-off: this chip states where the buffer is, where it lands and how long it is, and the other chip walks it eight bytes at a time and emits the commitment tuples.
+It is the only sender on that bus, which is what lets `MEMMOVE` decode the commitment functionality --- and with it the destination domain --- from the mere fact that it received the tuple.
+#render_constraint_table(chip, config, groups: "defer")
+
+Note that this chip therefore does not itself constrain the committed values, nor even see them, and that `index` is the only place where the two chips have to agree on more than the buffer: the verifier reconstructs the commitment side of the memory argument out of the committed output, so it is `index` that has to line up with the position of these bytes in that output.
+@commit:c:read_index is what makes it so, by advancing `x254` by exactly `count`.
+
+Lastly, we must make sure `μ` is a bit.
 #render_constraint_table(chip, config, groups: "bits")
 
 = Padding
 To pad this chip, use the below data.
 #render_chip_padding_table(chip, config)
 
+Every interaction in this chip is conditioned on `μ`, and the one constraint is satisfied by $#`μ` = 0$, so a padding row is all-zero.
+
 = Notes/optimizations
 - The current version only supports writing to `stdout`.
-  This chip could potentially be extended to support writing to arbitrary `fd`s
-- One might be able to replace @commit:c:end by `end => count = 0`.
-  While loosening the constraint (`count = 0 => end` is no longer enforced), this should not cause any problems:
-  if the prover does not set `end` when `count=0`, they simply cannot complete the proof.
-  First of all, one would have to recursively work through all $2^64$ values of `count`, something that is practically infeasible.
-  Moreover, if this is done with a sequence that originally has $#`count` > 0$, one will inevitably have to read a memory address twice at the same timestamp, which is impossible to prove.
-  In addition to dropping the `ZERO` lookup, this optimization might also permit moving `count_decr` from a `DWordHL` to a `DWordWL`, saving two columns.
-- Given that it is practically infeasible to commit more than $#`p`-1 = 2^64-2^32$ bytes in a program, it might suffice to store `count_decr` in a `BaseField`.
-  Note that this would probably involve having an extra (virtual) column storing `count` in `BaseField` form as well.
-  Moreover, one might need to add a lookup to `LT` to ensure $#`count` <= #`p`-1$ when being read from memory at the beginning of each commitment sequence.
+  This chip could potentially be extended to support writing to arbitrary `fd`s.
+- Nothing here bounds `count`, and neither does `MEMMOVE` on this path, so one `write` appends rows to that chip in proportion to its length.
+  That is a bound on prover cost only --- the commitment bus balances against the committed output, which the verifier knows in full --- but a `LT` lookup here, paired with chunking in the guest stub, would make the cost of a single system call bounded like every other one.
diff --git a/spec/chapters/memmove.typ b/spec/chapters/memmove.typ
new file mode 100644
index 000000000..5db5cda14
--- /dev/null
+++ b/spec/chapters/memmove.typ
@@ -0,0 +1,187 @@
+#import "/meta.typ": aside
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_variable_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  compute_nr_interactions,
+  render_constraint_table,
+  render_chip_assumptions,
+  render_chip_padding_table,
+)
+
+#let config = load_config()
+#let chip = load_chip("src/memmove.toml", config)
+#let memmove = raw(chip.name)
+
+The #memmove chip moves a range of bytes from one location to another, eight bytes per row.
+It is the only copying primitive of this VM: one chip serves `memcpy`, `memmove`, `memset` and the byte loop of a commitment.
+#footnote([Linux man-page on `memmove`; man7.org, version 6.16, 2025-10-29. #link("https://man7.org/linux/man-pages/man3/memmove.3.html")[[src]]])
+The three functionalities differ only in where the bytes go and in which of the two accesses happens first:
+
+#align(center)[#table(
+  columns: (auto, auto, auto, auto),
+  table.header("functionality", "entered from", "read at", "write at"),
+  [`memcpy`/`memmove`], `ECALL`,  $#`timestamp` + 1$, $#`timestamp` + 2$,
+  `memset`,           `ECALL`,  $#`timestamp` + 2$, $#`timestamp` + 1$,
+  `commit`,           `COMMIT`, $#`timestamp` + 1$, "the commitment domain",
+)]
+
+Neither the destination domain nor the order of the two accesses is chosen by the caller; both follow from `is_set` and `is_commit`, which are decoded from the way the sequence was entered.
+
+= Variables
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_interactions = compute_nr_interactions(chip)
+
+The #memmove chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
+#render_chip_variable_table(chip, config)
+
+= Assumptions
+#render_chip_assumptions(chip, config)
+
+These concern the _first_ row of a sequence, where the values come from the register file or from `COMMIT`; every later row receives them over `MEMMOVE_NEXT`, where @memmove:c:range_src_incr, @memmove:c:range_dst_incr, @memmove:c:range_src_incr_top, @memmove:c:range_dst_incr_top and @memmove:c:range_count_decr range-check three of the four on the sending side.
+Nothing range-checks `timestamp` on either side; it stays a `Word` only because it travels unchanged from the `ECALL` at the root of the sequence.
+On a commitment sequence nothing guarantees @memmove:a:dst at all (@memmove:aside:index).
+
+= Constraints
+In this VM, we assign syscall number -30 to the copy functionality of the #memmove accelerator, and -32 to `memset`.
+Since the number of bytes is not known in advance, this chip is recursive: each row moves one chunk and "calls" itself to move the remainder, so only the `first` row of a sequence accepts an entry.
+There are two entries --- an `ECALL` from the `CPU`, or the byte loop `COMMIT` defers (@commit) --- and `first_ecall` and `first_commit` split `first` between them.
+#render_constraint_table(chip, config, groups: "incoming")
+
+== Selecting the functionality
+@memmove:c:receive_ecall receives the system call number as $2^32 - 30 - 2 dot #`is_set`$, so `is_set` is decoded from the `ECALL` the guest executed rather than chosen.
+That number is a linear function of `is_set`, and the tuple's high limb is the constant $2^32 - 1$, so as `is_set` ranges over the whole field the pair reproduces _every_ system call number in the negative range.
+What rules those out is @memmove:c:range_is_set, which restricts `is_set` to $0$ and $1$ and so leaves only $-30$ and $-32$; it carries the whole decoding argument.
+`is_commit` is decoded instead from _which_ bus the first row accepted from, `COMMIT_DEFER` having exactly one sender.
+Both selectors ride inside the `MEMMOVE_NEXT` tuple in either direction, so a sequence cannot change functionality half way through it.
+#render_constraint_table(chip, config, groups: "functionality")
+
+The last three define nothing new --- they are a selector combined with `first`, with $#`μ` - #`end`$ and with `single` --- and exist as columns only because a multiplicity must be linear in the columns of the chip (@logup).
+
+== Reading the operands
+The guest-side `memcpy` this chip accelerates has the following signature:
+
+```c
+void *memcpy(size_t count; void dest[restrict count], const void src[restrict count], size_t count);
+```
+
+That is to say, `A0` contains the address of the first byte to write, `A1` the address of the first byte to read, and `A2` the number of bytes to move; `memset` uses the same three registers for the same three roles.
+Each read writes back the value it read, so the operation leaves the registers untouched and the guest produces the return value.
+These are conditioned on `first_ecall`, since a deferred commitment sequence takes its operands from `COMMIT_DEFER`.
+#render_constraint_table(chip, config, groups: "read_input")
+
+== Chunk width
+A row moves eight bytes, or a single byte when `single` is set.
+The width itself is left free --- the prover may cut any row to a single byte at any count --- but a wide row must have the bytes to fill it, and @memmove:c:wide_needs_eight is what asks for them: it puts $#`count` < 8$ to `LT` (@lt) and pins the answer to "no", at multiplicity $#`μ` - #`single`$.
+A wide row therefore fires the lookup and must have at least eight bytes left, while a narrow row does not fire it at all.
+Note that this obligation is carried by a lookup rather than by a polynomial, so there is no constraint in the table below that enforces it.
+That freedom decides which memory chip a row reaches: `MEMW_A` (@memw) admits an access that does not cross a $2^16$ limb boundary and whose bytes share one old timestamp, and a buffer last written in eight-byte groups has one timestamp per group, so a schedule can spend narrow rows to land its wide rows on those groups.
+@memmove:c:bound proves $#`count` < 257$ on the first row of every `ECALL`-entered sequence, capping it at $257$ rows; the guest stubs chunk larger operations.
+#render_constraint_table(chip, config, groups: "width")
+
+Note that @memmove:c:bound carries `first_ecall`, so a commitment sequence proves no byte bound, and `COMMIT` range-checks none either.
+No prover gain follows --- the commitment bus must balance against the committed output, which the verifier knows in full --- but the verifier contributes a token pair per committed byte, so an excessive `count` is unverifiable as well as unprovable.
+
+== Performing the move
+The bytes are read at $#`timestamp` + 1 + #`is_set`$ and written at $#`timestamp` + 2 - #`is_set`$, one timestamp apart, with `is_set` deciding which comes first.
+The `CPU`'s preprocessed timestamp column holds $4 dot (i + 1)$ at row $i$ (@vars), so neither expression leaves the `Word` range.
+Both interactions are expressed over the _same_ `value` variable, which is what makes the moved bytes equal, and the read carries `value` as input and output, pinning it to whatever the memory argument (@memory) holds at `src`.
+@memmove:c:single_lanes canonicalises a narrow row, whose seven unused lanes `MEMW` gates out of the memory argument but not out of its own tuple.
+#render_constraint_table(chip, config, groups: "copy")
+
+Every row of a sequence carries the same `timestamp`, so an entire sequence reads at one instant and writes at another.
+Under the normal order every read therefore observes memory as it was before the sequence started, which is `memmove`'s guarantee for an overlapping range; under the inverted order every read observes memory after all of the sequence's writes, and the sequence propagates rather than copies.
+That is `memset`: the guest seeds eight bytes with ordinary stores and calls with `src` the start of the seed and `dst` its end, and each row forces $"mem"[#`src` + k + 8] = "mem"[#`src` + k]$, replicating the seed across the range.
+
+@memmove:c:set_gap_lo and @memmove:c:set_gap_hi pin that gap, which is necessary: at $#`dst` = #`src`$ the read and the write address one cell at adjacent timestamps, the memory argument closes on $#`value` = #`value`$, and all eight lanes --- pinned by the read alone --- become free field elements.
+Only $#`dst` = #`src`$ frees them; the gap is $8$ because that is the widest row, so a wide row's read and write ranges stay disjoint.
+The gate is `is_set` alone rather than a product, which would cost a degree.
+Being limb-wise, the pair admits no carry out of the low limb, so a `memset` whose range crosses the $2^32$ boundary has no satisfying assignment at all --- a precondition on the caller, which the executor enforces.
+
+== Writing to the commitment domain
+The destination domain is the one thing `commit` changes about the write, and @memmove:c:write_value takes it straight from the selector: the domain it passes to `MEMW` is $2 dot #`is_commit`$, so a copy writes to RAM and a commitment writes to the domain-separated part of memory reserved for committed values (@memory).
+Nothing else differs --- same `value` lanes, same width flag, same multiplicity --- which is what lets one interaction serve both.
+
+The committed bytes therefore reach the memory argument as ordinary `MEMW` accesses, one token per byte at $#`dst` + i$, on `MEMW`'s rows rather than on this chip's.
+That the tokens are per byte is what decouples the verifier from the prover's row schedule: the verifier rebuilds this side of the bus from the committed output alone, where it sees only the concatenation of every commitment the program made, and the schedule restarts at every system call.
+`MEMW`'s width flags do the rest, so a narrow committing row writes the one byte it read and no more.
+
+The verifier initializes and finalizes this domain as it does any other (@memory, @streaming).#footnote[
+  In order to make sure the verifier can properly finalize the committed values, the last epoch can "bring forward" all commitments from earlier epochs, similar to padded values, in the `L2G` table.
+  Then the contribution of the commitments only consists of the tuples `(2, address, last_epoch_index, value)`, which is entirely known to the verifier.
+]
+
+#aside(ref: <memmove:aside:index>)[Note on the commitment index][
+  Nothing here guarantees @memmove:a:dst, and the reconstruction of `dst_incr_top` relies on it, so a denormalized index weakens the no-wraparound argument below to a field statement.
+  This is not a prover gain, since such a token has no receiver, but range-checking `index` where it enters `COMMIT` would settle it --- and would also stop @commit:c:read_index writing past the `Word` range into `x254`.
+]
+
+== Advancing to the next chunk
+In parallel, we compute $#`src_incr` = #`src` + #`step`$ and $#`dst_incr` = #`dst` + #`step`$ as the positions at which the next chunk starts, and $#`count_decr` = #`count` - #`step`$ as the number of bytes still to move.
+Only the low three halfwords of each position are stored: the fourth is reconstructed as `src_incr_top` and `dst_incr_top` from the carry out of the low limb, which is what @memmove:c:src_incr and @memmove:c:dst_incr pin to a bit.
+@memmove:c:range_count_decr is included to satisfy @sub:a:diff.
+#render_constraint_table(chip, config, groups: "incr_decr")
+
+The positions must not wrap modulo $2^64$, or a sequence could walk `src` past the end of the address space, or close into a ring that balances every bus while moving nothing that was asked for.
+No constraint says so. With the top halfword reconstructed, the relation it used to be pinned by holds by construction and would prove nothing; what carries the property instead are the range checks @memmove:c:range_src_incr_top and @memmove:c:range_dst_incr_top, together with the third halfword's.
+Both below $2^16$ is exactly $#`src`_1 + #`src_carry` < 2^32$, which is the no-wraparound statement.
+They are therefore load-bearing rather than bookkeeping.
+The count uses plain `SUB`, which permits it, because the terminal row holds $#`count` = 0$ and hence $#`count_decr` = 2^64 - 1$.
+That is safe because $#`step` <= #`count`$ on every active row with $#`count` >= 1$: a wide row is checked by @memmove:c:wide_needs_eight and hence has $#`count` >= 8 = #`step`$, and a narrow row has $#`step` = 1$.
+
+== Terminating the sequence
+When `count` hits $0$ we stop recursing, which the `end` bit indicates.
+#render_constraint_table(chip, config, groups: "end")
+
+*Note*:
++ We set $#`end` = 1$ when $#`count_decr` = -1$ rather than when $#`count` = 0$, which allows `count` to be stored in a `DWordWL` rather than a `DWordHL`.
++ $forall i in [0, 3]: 65535 - #`count_decr`_i >= 0$ as a result of @memmove:c:range_count_decr, hence $sum_(i=0)^3 65535 - #`count_decr`_i = 0 arrow.l.r.double.long forall i: #`count_decr`_i = 65535$.
+  Without those range checks one limb could compensate another and `end` would be claimable at a nonzero count --- a silently truncated operation with every bus balanced, since every memory interaction vanishes with `end`.
++ $#`end` = 1$ still forces $#`count` = 0$ even though the prover picks the width: the other candidate, $#`count` = 7$ with a wide row, is rejected by @memmove:c:wide_needs_eight.
++ An operation on zero bytes is a single row with $#`first` = #`end` = 1$.
+
+== Chaining the rows
+When this was not the last chunk, we recursively move the next one over `MEMMOVE_NEXT`, carrying the timestamp, the three updated values and the functionality.
+Both tuples carry the `timestamp`, which is what separates one sequence from another; since the CPU's timestamps strictly increase per instruction, no two sequences share one.
+This chip contributes the following to the lookup argument.
+#render_constraint_table(chip, config, groups: "lookups")
+
+Note that the two positions are sent as written-out expressions rather than as a packing of their columns, since their top halfword is not a column: the low element is $#`src_incr`_0 + 2^16 dot #`src_incr`_1$ and the high one is $#`src`_1 + #`src_carry`$, in which $#`src_incr`_2$ cancels. That halfword survives only to carry its range check.
+
+#aside("Why no termination constraint is needed")[
+  Fix a timestamp. Balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_commit`$ caps that at one, since the `CPU` sends one `ECALL` per timestamp and that `ECALL` cannot be both a copy and a `write`.
+  That rules out an _open_ sequence and nothing more: a ring of rows with neither `first` nor `end` set sends and receives one tuple each, so it balances while consuming no entry.
+  What forbids the ring is @memmove:c:range_src_incr_top: with no wraparound, $#`src_incr` = #`src` + #`step`$ holds over the integers with $#`step` >= 1$, so `src` strictly increases and can never return to a value it held.
+]
+
+== Bits
+Lastly, the six independent bits must be bits, and each of `first`, `end` and `single` must imply $#`μ` = 1$, to keep the multiplicities $-(#`μ` - #`first`)$, $#`μ` - #`end`$ and $#`μ` - #`single`$ binary.
+`first_ecall` needs no range check, being already equated to a product of bits.
+@memmove:c:single_implies_mu is worth singling out, since it looks like bookkeeping for the padding row and is not: at $#`μ` = 0$ with $#`single` = 1$ the width lookup would carry multiplicity $-1$, which would make this chip a _provider_ on the `ALU` bus and let any consumer take an unwitnessed $#`count` >= 8$ from it.
+#render_constraint_table(chip, config, groups: "bits")
+
+= Padding
+To pad this chip, use the below data.
+#render_chip_padding_table(chip, config)
+
+This padding row is not all-zero.
+@memmove:c:single_implies_mu forces $#`single` = 0$ here, so $#`step` = 8$; @memmove:c:count_decr is unconditional, which $#`count` = 8$ and $#`count_decr` = 0$ then satisfy.
+The low-limb carry of the two position updates is constrained on every row (@memmove:c:src_incr, @memmove:c:dst_incr), which $#`src_incr` = #`dst_incr` = 8$ satisfies with a zero carry.
+@memmove:c:wide_needs_eight is inert, its multiplicity being $0 - 0$.
+
+= The Accelerated Memory Operations standard
+The Ethereum Foundation's Accelerated Memory Operations standard fixes what an accelerated `memcpy`, `memmove` and `memset` must provide.
+#footnote([Accelerated Memory Operations; eth-act/zkevm-standards, commit `a97934c`, 2026-08-11. #link("https://github.com/eth-act/zkevm-standards/blob/a97934cae02693d3b69f07a7cd6e3ed6fb5e8053/standards/accelerated-memory-operations/README.md")[[src]]])
+Of the chip itself it asks that operands of arbitrary alignment be accepted, which they are: no constraint here refers to the alignment of `src`, `dst` or `count`, and a row's width is tied to none of them.
+The one restriction this chip does impose is not an alignment --- a `memset` may not straddle the $2^32$ limb boundary --- and the standard's fourth operation, `memcmp`, is not covered, as it does not copy.
+Its two remaining requirements fall outside this chapter: that the accelerated symbol behave identically to the C library function, which the guest stub is responsible for, and that it be a strong definition in an unconditionally linked object, which is a matter of linking.
+
+= Notes/optimizations
+- `count` need not be a full `DWordWL` on the `ECALL` path, where @memmove:c:bound already proves $#`count` < 257$; the commitment path has no such bound, so this costs a range check where the value enters from `COMMIT`.
+- The eight `IS_HALF` checks on the two positions carry multiplicity $#`μ`$ while `src_incr` and `dst_incr` are consumed only at $#`μ` - #`end`$. Lowering them would drop eight lookups per terminal row, though not shrink the proof, that table being preprocessed at a fixed height. They cannot be dropped altogether: two of the eight are the no-wraparound argument.
+- Selecting between exactly two widths keeps `single` a single bit, so $#`step` = 8 - 7 dot #`single`$ stays linear and, more to the point, so does @memmove:c:wide_needs_eight's multiplicity $#`μ` - #`single`$. With a two-bit selector the corresponding "fire only on the widest row" multiplicity is a product, and would need a gate column and a degree-2 constraint of its own, as `first_ecall` does. Four-, two- and one-byte chunks would save at most eight rows per sequence.
+- A row could move sixteen or thirty-two bytes, at the cost of a wider `MEMW` signature, but `MEMW_A` needs every byte of an access to share one old timestamp, which a wider row only manages where the buffer was written in groups at least that wide.
+- `COMMIT` could send its deferral on `MEMMOVE_NEXT` directly, retiring the `COMMIT_DEFER` bus and the `first_ecall` column, at the cost of `first` no longer meaning "head of the sequence" and of an added $#`first` dot #`is_commit` = 0$.
+- The `memmove` property belongs to one `ECALL`: past 256 bytes the stub splits into several at distinct timestamps, and chunk $k+1$ reads what chunk $k$ wrote. That is in-contract for `memcpy`, whose buffers may not overlap.
diff --git a/spec/meta.typ b/spec/meta.typ
index fc6bc783b..ee862f8ee 100644
--- a/spec/meta.typ
+++ b/spec/meta.typ
@@ -19,7 +19,7 @@
       ("is_bit", [`IS_BIT` template], <isbit>),
       ("is_byte", [`IS_BYTE` template], <isbyte>),
       ("sign", [`SIGN` template], <sign>),
-      ("add", [`ADD`/`SUB` template], <add>),
+      ("add", [`ADD`/`SUB`/`ADDNW` templates], <add>),
       ("neg", [`NEG` template], <neg>),
       ("reg", [`REG`/`REGW` template], <reg>),
     )),
@@ -51,6 +51,7 @@
       ("keccak", [`KECCAK` accelerator], <keccak>),
       ("ecsm", [`ECSM` accelerator], <ecsm>),
       ("fext", [Extension field accelerator], <fext>),
+      ("memmove", [`MEMMOVE` accelerator], <memmove>),
     )),
     ("MATHEMATICS", (
       ("limbs_and_carries", [On limb decomposition and carries], <limbs>),
diff --git a/spec/src/add_nw.toml b/spec/src/add_nw.toml
new file mode 100644
index 000000000..407767f12
--- /dev/null
+++ b/spec/src/add_nw.toml
@@ -0,0 +1,66 @@
+name = "ADDNW"
+
+# Variables
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "Whether the relation should be enforced ($eq.not 0$) or not ($0$)."
+
+[[variables.input]]
+name = "lhs"
+type = "DWordWL"
+desc = "left-hand operator"
+
+[[variables.input]]
+name = "rhs"
+type = "DWordWL"
+desc = "right-hand operator"
+
+[[variables.output]]
+name = "sum"
+type = "DWordWL"
+desc = "$#`lhs` + #`rhs`$"
+
+[[variables.virtual]]
+name = "carry"
+type = ["Bit", 2]
+desc = "Carry values used to constrain the addition"
+def = {idx="i", polys=[
+    {iter=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]},
+    {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 1], ["idx", "rhs", 1], ["idx", "carry", 0]], ["idx", "sum", 1]]]},
+]}
+
+# Assumptions
+
+[[assumptions]]
+desc = "`IS_WORD[lhs[i]]`"
+iter = ["i", 0, 1]
+ref = "addnw:a:lhs"
+
+[[assumptions]]
+desc = "`IS_WORD[rhs[i]]`"
+iter = ["i", 0, 1]
+ref = "addnw:a:rhs"
+
+[[assumptions]]
+desc = "`IS_WORD[sum[i]]`"
+iter = ["i", 0, 1]
+ref = "addnw:a:sum"
+
+# Constraints
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "template"
+tag = "IS_BIT"
+input = [["idx", "carry", 0]]
+ref = "addnw:c:carry"
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$#`cond` => #`carry`_1 = 0$"
+poly = ["*", "cond", ["idx", "carry", 1]]
+ref = "addnw:c:no_wraparound"
diff --git a/spec/src/commit.toml b/spec/src/commit.toml
index f6e77ffd8..73d3d347e 100644
--- a/spec/src/commit.toml
+++ b/spec/src/commit.toml
@@ -12,49 +12,19 @@ pad = 0
 [[variables.auxiliary]]
 name = "index"
 type = "BaseField"
-desc = "Index of value being committed."
+desc = "Index of the first value being committed by this sequence"
 pad = 0
 
 [[variables.auxiliary]]
 name = "address"
 type = "DWordWL"
-desc = "Address of first byte to commit."
+desc = "Address of first byte to commit"
 pad = 0
 
-[[variables.auxiliary]]
-name = "address_incr"
-type = "DWordHL"
-desc = "$#`address` + 1$"
-pad = 1
-
 [[variables.auxiliary]]
 name = "count"
 type = "DWordWL"
 desc = "number of bytes to commit"
-pad = 1
-
-[[variables.auxiliary]]
-name = "count_decr"
-type = "DWordHL"
-desc = "$#`count` - 1$"
-pad = ["arr", 0, 0, 0, 0]
-
-[[variables.auxiliary]]
-name = "first"
-type = "Bit"
-desc = "Whether this is the first commitment in this sequence."
-pad = 0
-
-[[variables.auxiliary]]
-name = "end"
-type = "Bit"
-desc = "Whether this is the end of the commitment sequence."
-pad = 0
-
-[[variables.auxiliary]]
-name = "value"
-type = "Byte"
-desc = "Byte stored at `address`."
 pad = 0
 
 [[variables.multiplicity]]
@@ -75,7 +45,7 @@ name = "incoming"
 kind = "interaction"
 tag = "ECALL"
 input = ["timestamp", ["cast", 64, "DWordWL"]]
-multiplicity = ["-", "first"]
+multiplicity = ["-", "μ"]
 ref = "commit:c:receive_ecall"
 
 [[constraint_groups]]
@@ -86,7 +56,7 @@ kind = "template"
 tag = "REG"
 input = [11, "address", "timestamp"]
 output = "address"
-cond = "first"
+cond = "μ"
 ref = "commit:c:read_address"
 
 [[constraints.read_input]]
@@ -94,7 +64,7 @@ kind = "template"
 tag = "REG"
 input = [12, "count", "timestamp"]
 output = "count"
-cond = "first"
+cond = "μ"
 ref = "commit:c:read_count"
 
 [[constraints.read_input]]
@@ -102,7 +72,7 @@ kind = "template"
 tag = "REG"
 input = [10, "count", "timestamp"]
 output = ["cast", 1, "DWordWL"]
-cond = "first"
+cond = "μ"
 ref = "commit:c:read_fd_write_count"
 
 [[constraints.read_input]]
@@ -110,120 +80,24 @@ kind = "template"
 tag = "REG"
 input = [254, ["arr", ["+", "index", ["cast", "count", "BaseField"]], 0], "timestamp"]
 output = ["arr", "index", 0]
-cond = "first"
+cond = "μ"
 ref = "commit:c:read_index"
 
-
-[[constraint_groups]]
-name = "incr_decr"
-
-[[constraints.incr_decr]]
-kind = "template"
-tag = "ADD"
-input = ["address", ["cast", 1, "DWordWL"]]
-output = ["cast", "address_incr", "DWordWL"]
-ref = "commit:c:address_incr"
-
-[[constraints.incr_decr]]
-kind = "interaction"
-tag = "IS_HALF"
-input = [["idx", "address_incr", "i"]]
-iter = ["i", 0, 3]
-multiplicity = "μ"
-ref = "commit:c:range_address_incr"
-
-[[constraints.incr_decr]]
-kind = "template"
-tag = "SUB"
-input = ["count", ["cast", 1, "DWordWL"]]
-output = ["cast", "count_decr", "DWordWL"]
-ref = "commit:c:count_decr"
-
-[[constraints.incr_decr]]
-kind = "interaction"
-tag = "IS_HALF"
-input = [["idx", "count_decr", "i"]]
-iter = ["i", 0, 3]
-multiplicity = "μ"
-ref = "commit:c:range_count_decr"
-
-
 [[constraint_groups]]
-name = "commit"
-
-[[constraints.commit]]
-kind = "interaction"
-tag = "MEMW"
-input = [0, "address", ["arr", "value", 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0]
-output = ["arr", "value", 0, 0, 0, 0, 0, 0, 0]
-multiplicity = ["-", "μ", "end"]
-ref = "commit:c:read_value"
+name = "defer"
 
-[[constraints.commit]]
+[[constraints.defer]]
 kind = "interaction"
-tag = "memory"
-input = [2, ["arr", "index", 0], 0, "value"]
-multiplicity = ["-", "μ", "end"]
-ref = "commit:c:commit_value_out"
-
-[[constraints.commit]]
-kind = "interaction"
-tag = "memory"
-input = [2, ["arr", "index", 0], 1, "value"]
-multiplicity = ["-", ["-", "μ", "end"]]
-ref = "commit:c:commit_value_in"
-
-[[constraint_groups]]
-name = "end"
-
-[[constraints.end]]
-kind = "interaction"
-tag = "ZERO"
-input = [["+", ["-", 0xFFFF, ["idx", "count_decr", 0]], ["-", 0xFFFF, ["idx", "count_decr", 1]], ["-", 0xFFFF, ["idx", "count_decr", 2]], ["-", 0xFFFF, ["idx", "count_decr", 3]]]]
-output = "end"
+tag = "COMMIT_DEFER"
+input = ["timestamp", "address", ["arr", "index", 0], "count"]
 multiplicity = "μ"
-ref = "commit:c:end"
+ref = "commit:c:defer_to_memmove"
 
 [[constraint_groups]]
 name = "bits"
 
-[[constraints.bits]]
-kind = "template"
-tag = "IS_BIT"
-input = ["first"]
-ref = "commit:c:range_first"
-
-[[constraints.bits]]
-kind = "template"
-tag = "IS_BIT"
-input = ["end"]
-ref = "commit:c:range_end"
-
 [[constraints.bits]]
 kind = "template"
 tag = "IS_BIT"
 input = ["μ"]
 ref = "commit:c:range_mu"
-
-[[constraints.bits]]
-kind = "arith"
-constraint = "$#`first` + #`end` => #`μ` = 1$"
-poly = ["*", ["+", "first", "end"], ["not", "μ"]]
-ref = "commit:c:first_or_end_implies_mu"
-
-[[constraint_groups]]
-name = "lookups"
-
-[[constraints.lookups]]
-kind = "interaction"
-tag = "CNB"
-input = ["timestamp", ["+", "index", 1], ["cast", "address_incr", "DWordWL"], ["cast", "count_decr", "DWordWL"]]
-multiplicity = ["-", "μ", "end"]
-ref = "commit:c:send_commit_next_byte"
-
-[[constraints.lookups]]
-kind = "interaction"
-tag = "CNB"
-input = ["timestamp", "index", "address", "count"]
-multiplicity = ["-", ["-", "μ", "first"]]
-ref = "commit:c:receive_commit_next_byte"
diff --git a/spec/src/memmove.toml b/spec/src/memmove.toml
new file mode 100644
index 000000000..002a2e8ae
--- /dev/null
+++ b/spec/src/memmove.toml
@@ -0,0 +1,419 @@
+name = "MEMMOVE"
+code = "MMV"
+
+# Input
+
+[[variables.input]]
+name = "timestamp"
+type = "Word"
+desc = "timestamp at which the operation is requested"
+pad = 0
+
+# Auxiliary
+
+[[variables.auxiliary]]
+name = "src"
+type = "DWordWL"
+desc = "Address of the first byte read by this row"
+pad = 0
+
+[[variables.auxiliary]]
+name = "src_incr"
+type = ["Half", 3]
+desc = "The low three halfwords of $#`src` + #`step`$; the top one is derived by #`src_incr_top`"
+pad = 8
+
+[[variables.auxiliary]]
+name = "dst"
+type = "DWordWL"
+desc = "Address of the first byte written by this row. For `commit`, the index of that byte in the committed output"
+pad = 0
+
+[[variables.auxiliary]]
+name = "dst_incr"
+type = ["Half", 3]
+desc = "The low three halfwords of $#`dst` + #`step`$; the top one is derived by #`dst_incr_top`"
+pad = 8
+
+[[variables.auxiliary]]
+name = "count"
+type = "DWordWL"
+desc = "Number of bytes that still have to be moved, including those moved by this row"
+pad = 8
+
+[[variables.auxiliary]]
+name = "count_decr"
+type = "DWordHL"
+desc = "$#`count` - #`step`$"
+pad = ["arr", 0, 0, 0, 0]
+
+[[variables.auxiliary]]
+name = "first"
+type = "Bit"
+desc = "Whether this is the first row of this sequence"
+pad = 0
+
+[[variables.auxiliary]]
+name = "end"
+type = "Bit"
+desc = "Whether this is the end of the sequence"
+pad = 0
+
+[[variables.auxiliary]]
+name = "single"
+type = "Bit"
+desc = "Whether this row moves a single byte rather than eight"
+pad = 0
+
+[[variables.auxiliary]]
+name = "is_set"
+type = "Bit"
+desc = "Whether this row runs the `memset` functionality, which inverts the order of the read and the write"
+pad = 0
+
+[[variables.auxiliary]]
+name = "is_commit"
+type = "Bit"
+desc = "Whether this row runs the `commit` functionality, which writes to the commitment domain rather than to RAM"
+pad = 0
+
+[[variables.auxiliary]]
+name = "first_ecall"
+type = "Bit"
+desc = "$#`first` dot (1 - #`is_commit`)$; whether this row is the first of a sequence entered through an `ECALL`"
+pad = 0
+
+[[variables.auxiliary]]
+name = "value"
+type = "DWordBL"
+desc = "The bytes moved by this row; only $#`value`_0$ is moved when $#`single` = 1$. Unconstrained on rows that move nothing"
+pad = 0
+
+# Virtual
+
+[[variables.virtual]]
+name = "step"
+type = "Byte"
+desc = "The stride this row advances by: eight, or one when `single` is set"
+def = ["-", 8, ["*", 7, "single"]]
+
+[[variables.virtual]]
+name = "src_carry"
+type = "Bit"
+desc = "Carry out of the least significant limb of $#`src` + #`step`$"
+def = ["*", ["^", 2, -32], ["-", ["+", ["idx", "src", 0], "step"], ["idx", "src_incr", 0], ["*", ["^", 2, 16], ["idx", "src_incr", 1]]]]
+
+[[variables.virtual]]
+name = "src_incr_top"
+type = "Half"
+desc = "The most significant halfword of $#`src` + #`step`$, reconstructed rather than stored"
+def = ["*", ["^", 2, -16], ["-", ["+", ["idx", "src", 1], "src_carry"], ["idx", "src_incr", 2]]]
+
+[[variables.virtual]]
+name = "dst_carry"
+type = "Bit"
+desc = "Carry out of the least significant limb of $#`dst` + #`step`$"
+def = ["*", ["^", 2, -32], ["-", ["+", ["idx", "dst", 0], "step"], ["idx", "dst_incr", 0], ["*", ["^", 2, 16], ["idx", "dst_incr", 1]]]]
+
+[[variables.virtual]]
+name = "dst_incr_top"
+type = "Half"
+desc = "The most significant halfword of $#`dst` + #`step`$, reconstructed rather than stored"
+def = ["*", ["^", 2, -16], ["-", ["+", ["idx", "dst", 1], "dst_carry"], ["idx", "dst_incr", 2]]]
+
+[[variables.virtual]]
+name = "first_commit"
+type = "Bit"
+desc = "$#`first` dot #`is_commit`$; whether this row is the first of a sequence deferred by `COMMIT`"
+def = ["-", "first", "first_ecall"]
+
+# Multiplicity
+
+[[variables.multiplicity]]
+name = "μ"
+type = "Bit"
+desc = ""
+pad = 0
+
+# Assumptions
+
+[[assumptions]]
+desc = "`IS_WORD[timestamp]`"
+ref = "memmove:a:timestamp"
+
+[[assumptions]]
+desc = "`IS_WORD[src[i]]`"
+iter = ["i", 0, 1]
+ref = "memmove:a:src"
+
+[[assumptions]]
+desc = "`IS_WORD[dst[i]]`"
+iter = ["i", 0, 1]
+ref = "memmove:a:dst"
+
+[[assumptions]]
+desc = "`IS_WORD[count[i]]`"
+iter = ["i", 0, 1]
+ref = "memmove:a:count"
+
+# Constraints
+
+[[constraint_groups]]
+name = "incoming"
+
+[[constraints.incoming]]
+kind = "interaction"
+tag = "ECALL"
+input = ["timestamp", ["arr", ["-", ["^", 2, 32], 30, ["*", 2, "is_set"]], ["-", ["^", 2, 32], 1]]]
+multiplicity = ["-", "first_ecall"]
+ref = "memmove:c:receive_ecall"
+
+[[constraints.incoming]]
+kind = "interaction"
+tag = "COMMIT_DEFER"
+input = ["timestamp", "src", "dst", "count"]
+multiplicity = ["-", "first_commit"]
+ref = "memmove:c:receive_commit_defer"
+
+[[constraint_groups]]
+name = "functionality"
+
+[[constraints.functionality]]
+kind = "arith"
+constraint = "$#`is_set` dot #`is_commit` = 0$"
+poly = ["*", "is_set", "is_commit"]
+ref = "memmove:c:one_hot"
+
+[[constraints.functionality]]
+kind = "arith"
+constraint = "$#`is_set` + #`is_commit` => #`μ` = 1$"
+poly = ["*", ["+", "is_set", "is_commit"], ["not", "μ"]]
+ref = "memmove:c:functionality_implies_mu"
+
+[[constraints.functionality]]
+kind = "arith"
+constraint = "$#`first_ecall` = #`first` dot (1 - #`is_commit`)$"
+poly = ["-", "first_ecall", ["*", "first", ["not", "is_commit"]]]
+ref = "memmove:c:first_ecall"
+
+[[constraint_groups]]
+name = "read_input"
+
+[[constraints.read_input]]
+kind = "template"
+tag = "REG"
+input = [10, "dst", "timestamp"]
+output = "dst"
+cond = "first_ecall"
+ref = "memmove:c:read_dst"
+
+[[constraints.read_input]]
+kind = "template"
+tag = "REG"
+input = [11, "src", "timestamp"]
+output = "src"
+cond = "first_ecall"
+ref = "memmove:c:read_src"
+
+[[constraints.read_input]]
+kind = "template"
+tag = "REG"
+input = [12, "count", "timestamp"]
+output = "count"
+cond = "first_ecall"
+ref = "memmove:c:read_count"
+
+[[constraint_groups]]
+name = "width"
+
+[[constraints.width]]
+kind = "interaction"
+tag = "ALU"
+input = ["count", ["cast", 8, "DWordWL"], ["opsel", "LT"]]
+output = ["arr", 0, 0]
+multiplicity = ["-", "μ", "single"]
+ref = "memmove:c:wide_needs_eight"
+
+[[constraints.width]]
+kind = "interaction"
+tag = "ALU"
+input = ["count", ["cast", 257, "DWordWL"], ["opsel", "LT"]]
+output = ["arr", 1, 0]
+multiplicity = "first_ecall"
+ref = "memmove:c:bound"
+
+[[constraint_groups]]
+name = "copy"
+
+[[constraints.copy]]
+kind = "interaction"
+tag = "MEMW"
+input = [0, "src", "value", ["+", "timestamp", 1, "is_set"], 0, 0, ["not", "single"]]
+output = "value"
+multiplicity = ["-", "μ", "end"]
+ref = "memmove:c:read_value"
+
+[[constraints.copy]]
+kind = "interaction"
+tag = "MEMW"
+input = [["*", 2, "is_commit"], "dst", "value", ["-", ["+", "timestamp", 2], "is_set"], 0, 0, ["not", "single"]]
+multiplicity = ["-", "μ", "end"]
+ref = "memmove:c:write_value"
+
+[[constraints.copy]]
+kind = "arith"
+constraint = "$#`single` => #`value`_i = 0$"
+poly = ["*", "single", ["idx", "value", "i"]]
+iter = ["i", 1, 7]
+ref = "memmove:c:single_lanes"
+
+[[constraints.copy]]
+kind = "arith"
+constraint = "$#`is_set` => #`dst`_0 = #`src`_0 + 8$"
+poly = ["*", "is_set", ["-", ["idx", "dst", 0], ["idx", "src", 0], 8]]
+ref = "memmove:c:set_gap_lo"
+
+[[constraints.copy]]
+kind = "arith"
+constraint = "$#`is_set` => #`dst`_1 = #`src`_1$"
+poly = ["*", "is_set", ["-", ["idx", "dst", 1], ["idx", "src", 1]]]
+ref = "memmove:c:set_gap_hi"
+
+[[constraint_groups]]
+name = "incr_decr"
+
+[[constraints.incr_decr]]
+kind = "template"
+tag = "IS_BIT"
+input = ["src_carry"]
+ref = "memmove:c:src_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "src_incr", "i"]]
+iter = ["i", 0, 2]
+multiplicity = "μ"
+ref = "memmove:c:range_src_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = ["src_incr_top"]
+multiplicity = "μ"
+ref = "memmove:c:range_src_incr_top"
+
+[[constraints.incr_decr]]
+kind = "template"
+tag = "IS_BIT"
+input = ["dst_carry"]
+ref = "memmove:c:dst_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "dst_incr", "i"]]
+iter = ["i", 0, 2]
+multiplicity = "μ"
+ref = "memmove:c:range_dst_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = ["dst_incr_top"]
+multiplicity = "μ"
+ref = "memmove:c:range_dst_incr_top"
+
+[[constraints.incr_decr]]
+kind = "template"
+tag = "SUB"
+input = ["count", ["arr", "step", 0]]
+output = ["cast", "count_decr", "DWordWL"]
+ref = "memmove:c:count_decr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "count_decr", "i"]]
+iter = ["i", 0, 3]
+multiplicity = "μ"
+ref = "memmove:c:range_count_decr"
+
+[[constraint_groups]]
+name = "end"
+
+[[constraints.end]]
+kind = "interaction"
+tag = "ZERO"
+input = [["+", ["-", 0xFFFF, ["idx", "count_decr", 0]], ["-", 0xFFFF, ["idx", "count_decr", 1]], ["-", 0xFFFF, ["idx", "count_decr", 2]], ["-", 0xFFFF, ["idx", "count_decr", 3]]]]
+output = "end"
+multiplicity = "μ"
+ref = "memmove:c:end"
+
+[[constraint_groups]]
+name = "bits"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["first"]
+ref = "memmove:c:range_first"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["end"]
+ref = "memmove:c:range_end"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["single"]
+ref = "memmove:c:range_single"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["is_set"]
+ref = "memmove:c:range_is_set"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["is_commit"]
+ref = "memmove:c:range_is_commit"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["μ"]
+ref = "memmove:c:range_mu"
+
+[[constraints.bits]]
+kind = "arith"
+constraint = "$#`single` => #`μ` = 1$"
+poly = ["*", "single", ["not", "μ"]]
+ref = "memmove:c:single_implies_mu"
+
+[[constraints.bits]]
+kind = "arith"
+constraint = "$#`first` + #`end` => #`μ` = 1$"
+poly = ["*", ["+", "first", "end"], ["not", "μ"]]
+ref = "memmove:c:first_or_end_implies_mu"
+
+[[constraint_groups]]
+name = "lookups"
+
+[[constraints.lookups]]
+kind = "interaction"
+tag = "MEMMOVE_NEXT"
+input = ["timestamp", ["arr", ["+", ["idx", "src_incr", 0], ["*", ["^", 2, 16], ["idx", "src_incr", 1]]], ["+", ["idx", "src", 1], "src_carry"]], ["arr", ["+", ["idx", "dst_incr", 0], ["*", ["^", 2, 16], ["idx", "dst_incr", 1]]], ["+", ["idx", "dst", 1], "dst_carry"]], ["cast", "count_decr", "DWordWL"], "is_set", "is_commit"]
+multiplicity = ["-", "μ", "end"]
+ref = "memmove:c:send_next_chunk"
+
+[[constraints.lookups]]
+kind = "interaction"
+tag = "MEMMOVE_NEXT"
+input = ["timestamp", "src", "dst", "count", "is_set", "is_commit"]
+multiplicity = ["-", ["-", "μ", "first"]]
+ref = "memmove:c:receive_next_chunk"
diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml
index bdc85f9bf..72b093023 100644
--- a/spec/src/signatures.toml
+++ b/spec/src/signatures.toml
@@ -28,6 +28,14 @@ input = ["DWordWL", "DWordWL"]
 output = "DWordWL"
 cond = "BaseField"
 
+# cond => ADDNW<sum; lhs, rhs>
+[[signatures]]
+tag = "ADDNW"
+kind = "template"
+input = ["DWordWL", "DWordWL"]
+output = "DWordWL"
+cond = "BaseField"
+
 # cond => NEG<neg; X>
 [[signatures]]
 tag = "NEG"
@@ -118,11 +126,17 @@ tag = "ECALL"
 kind = "interaction"
 input = ["Word", "DWordWL"]
 
-# CNB[timestamp, index, address, count]
+# COMMIT_DEFER[timestamp, src, dst, count]
+[[signatures]]
+tag = "COMMIT_DEFER"
+kind = "interaction"
+input = ["Word", "DWordWL", "DWordWL", "DWordWL"]
+
+# MEMMOVE_NEXT[timestamp, src, dst, count, is_set, is_commit]
 [[signatures]]
-tag = "CNB"
+tag = "MEMMOVE_NEXT"
 kind = "interaction"
-input = ["Word", "BaseField", "DWordWL", "DWordWL"]
+input = ["Word", "DWordWL", "DWordWL", "DWordWL", "Bit", "Bit"]
 
 # BYTE_ALU[res; selector, X, Y]
 [[signatures]]