spec: DMA memcpy accelerator

spec/about_ecalls.typ

@@ -32,6 +32,7 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our
 / 93: `exit` (@halt)
 / -1: `SHA256` (@sha256)
 / -2: `KECCAK` (@keccak)
+/ -3: `DMA`/`memcpy` (@dma)
 / -11: `ECSM`/`secp256k1` (@ecsm)
 / -12: `ECSM`/`secp256r1` (@ecsm)
 / -20: `FEXT_LOAD` (@fext)

spec/add.typ

@@ -5,14 +5,17 @@
 #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)
 
 #show: book-page(chip.name)
 
 #set_nr_interactions(chip, name: "SUB")
+#set_nr_interactions(chip, name: "ADDNW")
 #let nr_interactions = compute_nr_interactions(chip)
 
 #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.
@@ -52,3 +55,24 @@ 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 additionally 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.
+
+The relation itself is delegated to #add; all #addnw adds is that the carry out of the most significant limb vanishes.
+
+== Variables
+This template introduces #nr_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$.

spec/book.typ

@@ -52,6 +52,7 @@
       ("commit.typ", [`COMMIT` chip], <commit>),
       ("sha256.typ", [`SHA256` accelerator], <sha256>),
       ("keccak.typ", [`KECCAK` accelerator], <keccak>),
+      ("dma.typ", [`DMA` accelerator], <dma>),
       ("ecsm.typ", [`ECSM` accelerator], <ecsm>),
       ("fext.typ", [Extension field accelerator], <fext>),
     )),

spec/dma.typ

@@ -0,0 +1,158 @@
+#import "/book.typ": book-page, 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,
+)
+
+#show: book-page("dma.typ")
+
+#let config = load_config()
+#let chip = load_chip("src/dma.toml", config)
+#let dma = raw(chip.name)
+
+The #dma chip copies a range of bytes from one location in memory to another, that is, it performs a `memcpy`.
+#footnote([Linux man-page on `memcpy`; man7.org, version 6.16, 2025-10-29. #link("https://man7.org/linux/man-pages/man3/memcpy.3.html")[[src]]])
+The guest performs such a copy with a RISC-V loop --- per copied word a load, a store, two pointer increments and a branch, each of them a `CPU` row (@cpu) together with its memory operations.
+This accelerator replaces all of that with a single row per eight copied bytes.
+
+= 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 #dma chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interactions:
+#render_chip_variable_table(chip, config)
+
+= Assumptions
+#render_chip_assumptions(chip, config)
+
+Note that these assumptions concern the _first_ row of a copy sequence only:
+every subsequent row receives `src`, `dst` and `count` over the `DMA_NEXT` bus, whose sender range-checks all three (@dma:c:range_src_incr, @dma:c:range_dst_incr and @dma:c:range_count_decr).
+
+= Constraints
+In this VM, we assign system call number $-3$ to the #dma accelerator.
+Since we do not know how many bytes are to be copied, this chip employs the same recursive design as `COMMIT` (@commit):
+each iteration copies one chunk of bytes, and recursively "calls" itself to copy the remainder.
+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.
+#render_constraint_table(chip, config, groups: "incoming")
+
+The `memcpy` operation has the following signature:
+
+```c
+void *memcpy(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` contains the address of the first byte to read, and
+- `A2` contains `count`.
+
+@dma:c:read_dst, @dma:c:read_src and @dma:c:read_count read these three registers.
+Each of them writes back the value that was read, so the copy leaves the registers untouched;
+the guest is responsible for producing `memcpy`'s return value.
+Again, these memory interactions only take place when this is the `first` call in the recursion tree.
+#render_constraint_table(chip, config, groups: "read_input")
+
+== Chunk width
+A row copies eight bytes whenever at least eight bytes remain, and a single byte otherwise.
+@dma:c:tail pins that choice to `LT` (@lt): the prover cannot select a convenient partition of the requested range.
+A copy of $n$ bytes is therefore laid out as $floor(n \/ 8)$ eight-byte rows, followed by $n mod 8$ one-byte rows, followed by one terminal row.
+
+Because a row is the unit in which this chip charges for a copy, an unbounded `count` would let a single guest instruction append an unbounded number of rows to the trace.
+@dma:c:bound therefore proves $#`count` < 257$ on the first row of every sequence.
+The guest-side `memcpy` chunks larger copies into multiple `ECALL`s; the executor rejects any chunk exceeding 256 bytes.
+#render_constraint_table(chip, config, groups: "width")
+
+#aside("Why a one-byte tail")[
+  Selecting between exactly two widths lets `tail` be a single bit, so $#`step` = 8 - 7 dot #`tail`$ stays linear and every constraint in this chip stays of degree 2.
+  Splitting the remainder into four-, two- and one-byte chunks instead would shave off at most four rows per sequence, at the cost of a two-bit width selector and a decoding of that selector into `MEMW`'s `write2`/`write4`/`write8` flags.
+]
+
+== Performing the copy
+The bytes are read from `src` at $#`timestamp` + 1$ and written to `dst` at $#`timestamp` + 2$.
+Both interactions are expressed over the _same_ `value` variable, which is what makes the copied bytes equal:
+there is nothing to constrain, since there is only one set of columns.
+The read carries `value` as both its input and its output, so `value` is pinned to whatever the memory argument (@memory) says resides at `src`.
+
+Splitting the two accesses over two consecutive timestamps is what gives an overlapping copy well-defined semantics:
+the memory argument orders accesses to an address by timestamp, so _every_ read of this `ECALL` observes memory as it was before the copy started.
+A single `ECALL` hence behaves like `memmove` rather than like a byte-by-byte forward copy.
+
+#render_constraint_table(chip, config, groups: "copy")
+
+@dma:c:tail_lanes is what keeps a one-byte row honest.
+Such a row addresses `MEMW` with $#`write2` = #`write4` = #`write8` = 0$, i.e. it presents a single-byte access;
+the seven unused lanes of `value` must then be zero, as they would otherwise carry unconstrained field elements onto the memory bus.
+
+== Advancing to the next chunk
+In parallel, we compute $#`src_incr` = #`src` + #`step`$ and $#`dst_incr` = #`dst` + #`step`$ as the addresses at which the next chunk starts, and $#`count_decr` = #`count` - #`step`$ as the number of bytes that still have to be copied afterwards.
+@dma:c:range_src_incr, @dma:c:range_dst_incr and @dma:c:range_count_decr are included to satisfy @addnw:a:sum respectively @sub:a:diff.
+#render_constraint_table(chip, config, groups: "incr_decr")
+
+Note the asymmetry between the two address updates and the count update:
+
++ The addresses use `ADDNW` (@add), which forbids wraparound modulo $2^64$.
+  Without it a sequence could walk `src` past the end of the address space and continue at low addresses, touching memory unrelated to the requested range.
+  The condition is $#`μ` - #`end`$: on the terminal row and on padding rows the computed successor is consumed by nobody, since @dma:c:send_copy_next_chunk carries that same multiplicity.
++ The count uses plain `SUB` (@add), which permits wraparound, because the terminal row holds $#`count` = 0$ and hence $#`count_decr` = 0 - 1 = 2^64 - 1$.
+  That permission is safe precisely because @dma:c:tail pins $#`tail` = (#`count` < 8)$, so $#`step` <= #`count`$ on every row with $#`count` >= 1$ and the subtraction can only wrap on the terminal row.
+  Dropping the pin would make $#`count` = 7$ with $#`tail` = 0$ acceptable, which wraps `count_decr` and thus claims `end` while seven requested bytes were never copied.
+
+== Terminating the sequence
+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*:
++ As in `COMMIT` (@commit), 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 @dma: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
+  $
+  Without those range checks the sum could reach $4 dot 65535$ for a `count_decr` other than $2^64 - 1$, and `end` would be claimable at a nonzero count.
+  That matters more here than the shape of the constraint suggests: since both memory interactions carry multiplicity $#`μ` - #`end`$, a row that wrongly claims `end` emits no memory operations at all, which is a silently truncated copy with every bus balanced.
++ A copy of zero bytes is a single row with $#`first` = #`end` = 1$: it accepts the `ECALL` and reads the three registers, but emits no memory operations and starts no recursion.
+
+== Chaining the rows
+When this was not the last chunk of this sequence, we recursively copy the next chunk over the `DMA_NEXT` bus, specifying the timestamp, the addresses to continue reading and writing at, and the number of bytes that still have to be copied (@dma:c:send_copy_next_chunk).
+Since that certainly won't be the `first` call in the sequence, we read `src_incr`, `dst_incr` and `count_decr` from the previous recursion level into `src`, `dst` and `count`, and continue copying.
+#render_constraint_table(chip, config, groups: "lookups")
+
+Both tuples carry the `timestamp`, and that is what separates one copy from another:
+without it, rows belonging to two different copies could be spliced into each other's sequences while the bus still balances.
+Since the CPU's timestamps strictly increase per instruction, no two #dma `ECALL`s share one.
+
+Observe also that this chip has no constraint demanding that a sequence terminates.
+It does not need one: a sequence without a terminal row sends one `DMA_NEXT` tuple more than it receives, and the bus does not balance.
+
+== Bits
+Lastly, we must make sure `first`, `end`, `tail` and `μ` are bits, and that either $#`first` = 1$ or $#`end` = 1$ implies $#`μ` = 1$ (@dma:c:first_or_end_implies_mu).
+The latter is required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary.
+#render_constraint_table(chip, config, groups: "bits")
+
+= Padding
+To pad this chip, use the below data.
+#render_chip_padding_table(chip, config)
+
+Note that this padding row is not all-zero.
+@dma:c:count_decr is unconditional, so a padding row has to satisfy it too: $#`tail` = 1$ makes $#`step` = 1$, which $#`count` = 1$ and $#`count_decr` = 0$ then satisfy.
+The two address updates carry the condition $#`μ` - #`end`$ and hence impose nothing on a padding row.
+Assigning them $#`src_incr` = #`dst_incr` = 1$ anyway keeps a padding row a well-formed inactive one-byte step, rather than one that merely happens to be unconstrained.
+
+= Notes/optimizations
+- The copy is a `memmove` per `ECALL`, but _not_ per guest-level `memcpy`: a copy larger than 256 bytes is chunked into several `ECALL`s at distinct timestamps, and chunk $k+1$ reads what chunk $k$ has already written.
+  This is in-contract for `memcpy`, whose buffers may not overlap, but the `memmove` property must not be claimed at the guest level.
+- The `value` variable is typed as bytes, but this chip range-checks none of its lanes.
+  They are pinned by @dma:c:read_value instead: a lane holds whatever the memory argument says resides at that address.
+  Only the seven lanes that a one-byte row leaves unused need @dma:c:tail_lanes, since those never reach the read.
+- `count` need not be a full `DWordWL`: @dma:c:bound already proves $#`count` < 257$ on the first row of a sequence, and every later `count` is smaller still.
+  Representing it as a single `Word`, or even as a `Half`, would save a column and shrink both `LT` interactions --- at the cost of an extra range check where the value enters from the register.
+- A row could copy sixteen or thirty-two bytes rather than eight, at the cost of a wider `MEMW` signature.
+  The number of rows for a maximal copy would drop from 33 to 17 respectively 9.

spec/src/add_nw.toml

@@ -0,0 +1,68 @@
+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 = "ADD"
+input = ["lhs", "rhs"]
+output = "sum"
+cond = "cond"
+ref = "addnw:c:add"
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$#`cond` => #`carry`_1 = 0$"
+poly = ["*", "cond", ["idx", "carry", 1]]
+ref = "addnw:c:no_wraparound"