Spec: unified MEMMOVE accelerator

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)

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.

spec/chapters/commit.typ

@@ -1,35 +1,32 @@
-#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/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,84 +38,43 @@ 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`.
 
 @commit:c:read_address reads `address` from `x11` (=`A1`) and @commit:c:read_count reads `count` from `x12` (=`A2`).
 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.