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..60037f202
--- /dev/null
+++ b/spec/chapters/memmove.typ
@@ -0,0 +1,173 @@
+#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 and @memmove:c:range_count_decr range-check three of the four on the sending side.
+`timestamp` is range-checked by neither side and holds only because it travels unchanged from the `ECALL` at the root.
+@memmove:a:dst is not discharged at all on a commitment sequence (@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.
+Note that the low limb of that tuple is a line in `is_set` and so reaches every system call number in the negative range: @memmove:c:range_is_set is what excludes them, and it therefore 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 `tail` --- 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`.
+#render_constraint_table(chip, config, groups: "read_input")
+
+== Chunk width
+A row moves eight bytes, or a single byte when `tail` is set.
+@memmove:c:short pins $#`count_lt8` = (#`count` < 8)$ to `LT` (@lt) and @memmove:c:wide_needs_eight forbids a wide row when fewer than eight bytes remain; the other direction is deliberately free, so the prover may cut any row to a single byte.
+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:tail_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
+When `is_commit` is set, `dst` is the index of the byte in the committed output rather than an address, and the write goes to a domain-separated part of memory with separator $2$, which the verifier initializes and finalizes itself (@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.
+]
+@memmove:c:write_value is gated on `ram_write` and does not fire; these take its place, and need no `MEMW`, since a commitment cell is written once and read by nobody.
+#render_constraint_table(chip, config, groups: "commit")
+
+#aside(ref: <memmove:aside:index>)[Note on the commitment index][
+  @memmove:a:dst is undischarged here, and @memmove:c:dst_incr leans on it through @addnw:a:lhs, so a denormalized index weakens that `ADDNW` to a field statement; the per-lane addresses below are likewise not carry-normalized as `MEMW`'s are.
+  Neither is a prover gain, since such a token has no receiver, but range-checking `index` where it enters `COMMIT` would settle both --- and would also stop @commit:c:read_index writing past the `Word` range into `x254`.
+]
+
+A committing row emits one interaction per _byte_, at index $#`dst` + i$, because the verifier rebuilds this side of the bus from the committed output alone and cannot reproduce the prover's row schedule, which restarts at every system call.
+Addressing every byte by its own index removes the grouping; `commit_lane` keeps a narrow row from committing the seven bytes it never read.
+
+== 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.
+The first two of @memmove:c:range_src_incr, @memmove:c:range_dst_incr and @memmove:c:range_count_decr are included to satisfy @addnw:a:sum, and the last to satisfy @sub:a:diff.
+#render_constraint_table(chip, config, groups: "incr_decr")
+
+The positions use `ADDNW` (@add), which forbids wraparound modulo $2^64$: without it 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.
+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 row with $#`count` >= 1$: a wide row needs $#`count_lt8` = 0$ and hence $#`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, gives $#`count_lt8` = 1$ and 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")
+
+#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:src_incr, since `ADDNW` forces $#`src_incr` = #`src` + #`step`$ over the integers with $#`step` >= 1$, so `src` strictly increases and can never return to a value it held.
+]
+
+== Bits
+Lastly, the seven independent bits must be bits, and $#`first` = 1$ or $#`end` = 1$ must imply $#`μ` = 1$, to keep the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ binary.
+`first_ecall`, `commit_write` and `commit_write_wide` need no range check, being already equated to products of bits.
+#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:count_decr is unconditional, so $#`tail` = 1$ makes $#`step` = 1$, which $#`count` = 1$ and $#`count_decr` = 0$ satisfy, and $#`tail` = 1$ also satisfies @memmove:c:wide_needs_eight.
+The low-limb carry of the two position updates is constrained on every row (@addnw:c:carry), which $#`src_incr` = #`dst_incr` = 1$ satisfies with a zero carry.
+
+= 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 `e6a4cc0`. #link("https://github.com/eth-act/zkevm-standards/tree/e6a4cc0/standards/accelerated-memory-operations")[[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`.
+- @memmove:c:range_src_incr and @memmove:c:range_dst_incr carry multiplicity $#`μ`$ while `src_incr` and `dst_incr` are consumed only at $#`μ` - #`end`$. Lowering both would drop eight `IS_HALF` lookups per terminal row, though not shrink the proof, that table being preprocessed at a fixed height.
+- Selecting between exactly two widths keeps `tail` a single bit, so $#`step` = 8 - 7 dot #`tail`$ stays linear and every constraint stays of degree 2. Four-, two- and one-byte chunks would save at most eight rows per sequence, at the cost of a two-bit selector.
+- 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..bf25e244d
--- /dev/null
+++ b/spec/src/memmove.toml
@@ -0,0 +1,455 @@
+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 = "DWordHL"
+desc = "$#`src` + #`step`$"
+pad = 1
+
+[[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 = "DWordHL"
+desc = "$#`dst` + #`step`$"
+pad = 1
+
+[[variables.auxiliary]]
+name = "count"
+type = "DWordWL"
+desc = "Number of bytes that still have to be moved, including those moved by this row"
+pad = 1
+
+[[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 = "tail"
+type = "Bit"
+desc = "Whether this row moves a single byte rather than eight"
+pad = 1
+
+[[variables.auxiliary]]
+name = "count_lt8"
+type = "Bit"
+desc = "Whether $#`count` < 8$, i.e. whether this row may not move eight bytes"
+pad = 1
+
+[[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 = "commit_write"
+type = "Bit"
+desc = "$(#`μ` - #`end`) dot #`is_commit`$; whether this row writes to the commitment domain"
+pad = 0
+
+[[variables.auxiliary]]
+name = "commit_write_wide"
+type = "Bit"
+desc = "$#`commit_write` dot (1 - #`tail`)$; whether this row writes eight bytes to the commitment domain"
+pad = 0
+
+[[variables.auxiliary]]
+name = "value"
+type = "DWordBL"
+desc = "The bytes moved by this row; only $#`value`_0$ is moved when $#`tail` = 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 `tail` is set"
+def = ["-", 8, ["*", 7, "tail"]]
+
+[[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"]
+
+[[variables.virtual]]
+name = "ram_write"
+type = "Bit"
+desc = "$(#`μ` - #`end`) dot (1 - #`is_commit`)$; whether this row writes to RAM"
+def = ["-", "μ", "end", "commit_write"]
+
+[[variables.virtual]]
+name = "commit_lane"
+type = ["Bit", 8]
+desc = "Whether lane $i$ reaches the commitment domain: lane $0$ on every committing row, lanes $1$ through $7$ only on a wide one"
+def = {idx = "i", polys = [
+    {iter = 0, poly = "commit_write"},
+    {iter = [1, 7], poly = "commit_write_wide"},
+]}
+
+# 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"
+
+[[constraints.functionality]]
+kind = "arith"
+constraint = "$#`commit_write` = (#`μ` - #`end`) dot #`is_commit`$"
+poly = ["-", "commit_write", ["*", ["-", "μ", "end"], "is_commit"]]
+ref = "memmove:c:commit_write"
+
+[[constraints.functionality]]
+kind = "arith"
+constraint = "$#`commit_write_wide` = #`commit_write` dot (1 - #`tail`)$"
+poly = ["-", "commit_write_wide", ["*", "commit_write", ["not", "tail"]]]
+ref = "memmove:c:commit_write_wide"
+
+[[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", "count_lt8", 0]
+multiplicity = "μ"
+ref = "memmove:c:short"
+
+[[constraints.width]]
+kind = "arith"
+constraint = "$#`count_lt8` => #`tail` = 1$"
+poly = ["*", ["not", "tail"], "count_lt8"]
+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", "tail"]]
+output = "value"
+multiplicity = ["-", "μ", "end"]
+ref = "memmove:c:read_value"
+
+[[constraints.copy]]
+kind = "interaction"
+tag = "MEMW"
+input = [0, "dst", "value", ["-", ["+", "timestamp", 2], "is_set"], 0, 0, ["not", "tail"]]
+multiplicity = "ram_write"
+ref = "memmove:c:write_value"
+
+[[constraints.copy]]
+kind = "arith"
+constraint = "$#`tail` => #`value`_i = 0$"
+poly = ["*", "tail", ["idx", "value", "i"]]
+iter = ["i", 1, 7]
+ref = "memmove:c:tail_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 = "commit"
+
+[[constraints.commit]]
+kind = "interaction"
+tag = "memory"
+input = [2, ["arr", ["+", ["idx", "dst", 0], "i"], ["idx", "dst", 1]], 0, ["idx", "value", "i"]]
+iter = ["i", 0, 7]
+multiplicity = ["idx", "commit_lane", "i"]
+ref = "memmove:c:commit_value_out"
+
+[[constraints.commit]]
+kind = "interaction"
+tag = "memory"
+input = [2, ["arr", ["+", ["idx", "dst", 0], "i"], ["idx", "dst", 1]], 1, ["idx", "value", "i"]]
+iter = ["i", 0, 7]
+multiplicity = ["-", ["idx", "commit_lane", "i"]]
+ref = "memmove:c:commit_value_in"
+
+[[constraint_groups]]
+name = "incr_decr"
+
+[[constraints.incr_decr]]
+kind = "template"
+tag = "ADDNW"
+input = ["src", ["arr", "step", 0]]
+output = ["cast", "src_incr", "DWordWL"]
+cond = ["-", "μ", "end"]
+ref = "memmove:c:src_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "src_incr", "i"]]
+iter = ["i", 0, 3]
+multiplicity = "μ"
+ref = "memmove:c:range_src_incr"
+
+[[constraints.incr_decr]]
+kind = "template"
+tag = "ADDNW"
+input = ["dst", ["arr", "step", 0]]
+output = ["cast", "dst_incr", "DWordWL"]
+cond = ["-", "μ", "end"]
+ref = "memmove:c:dst_incr"
+
+[[constraints.incr_decr]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "dst_incr", "i"]]
+iter = ["i", 0, 3]
+multiplicity = "μ"
+ref = "memmove:c:range_dst_incr"
+
+[[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 = ["tail"]
+ref = "memmove:c:range_tail"
+
+[[constraints.bits]]
+kind = "template"
+tag = "IS_BIT"
+input = ["count_lt8"]
+ref = "memmove:c:range_count_lt8"
+
+[[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 = "$#`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", ["cast", "src_incr", "DWordWL"], ["cast", "dst_incr", "DWordWL"], ["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]]