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")
 #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.
@@ -52,3 +55,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.
+
+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.
+
+== 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$.

spec/book.typ

@@ -22,7 +22,7 @@
       ("is_bit.typ", [`IS_BIT` template], <isbit>),
       ("is_byte.typ", [`IS_BYTE` template], <isbyte>),
       ("sign.typ", [`SIGN` template], <sign>),
-      ("add.typ", [`ADD`/`SUB` template], <add>),
+      ("add.typ", [`ADD`/`SUB`/`ADDNW` templates], <add>),
       ("neg.typ", [`NEG` template], <neg>),
       ("reg.typ", [`REG`/`REGW` template], <reg>),
     )),
@@ -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/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"