From 4a39c3835c0c9298d9bfcdcc6b9bc2ff2ee15885 Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 11 Aug 2026 16:28:19 -0300 Subject: [PATCH 1/4] Add DMA memcpy accelerator to the spec --- spec/about_ecalls.typ | 1 + spec/add.typ | 24 ++++ spec/book.typ | 1 + spec/dma.typ | 156 ++++++++++++++++++++ spec/src/add_nw.toml | 68 +++++++++ spec/src/dma.toml | 303 +++++++++++++++++++++++++++++++++++++++ spec/src/signatures.toml | 14 ++ 7 files changed, 567 insertions(+) create mode 100644 spec/dma.typ create mode 100644 spec/src/add_nw.toml create mode 100644 spec/src/dma.toml diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index f4ae00a23..ac3865925 100644 --- a/spec/about_ecalls.typ +++ b/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) diff --git a/spec/add.typ b/spec/add.typ index 1f597c083..386d52d2a 100644 --- a/spec/add.typ +++ b/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$. diff --git a/spec/book.typ b/spec/book.typ index 052f134bd..34a466fb0 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -52,6 +52,7 @@ ("commit.typ", [`COMMIT` chip], ), ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), + ("dma.typ", [`DMA` accelerator], ), ("ecsm.typ", [`ECSM` accelerator], ), ("fext.typ", [Extension field accelerator], ), )), diff --git a/spec/dma.typ b/spec/dma.typ new file mode 100644 index 000000000..652973310 --- /dev/null +++ b/spec/dma.typ @@ -0,0 +1,156 @@ +#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 leverages #nr_variables variables, spanning #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 three 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. + +== 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: $#`tail` = 1$ makes $#`step` = 1$, which $#`count` = 1$ and $#`count_decr` = 0$ then satisfy. +The same holds for the two address updates, whence $#`src_incr` = #`dst_incr` = 1$. + += 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. diff --git a/spec/src/add_nw.toml b/spec/src/add_nw.toml new file mode 100644 index 000000000..ef86adeec --- /dev/null +++ b/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" diff --git a/spec/src/dma.toml b/spec/src/dma.toml new file mode 100644 index 000000000..7ddf2c52d --- /dev/null +++ b/spec/src/dma.toml @@ -0,0 +1,303 @@ +name = "DMA" +code = "DMA" + +# Input + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "timestamp at which the copy 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." +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 copied, including those copied 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 copy sequence." +pad = 0 + +[[variables.auxiliary]] +name = "end" +type = "Bit" +desc = "Whether this is the end of the copy sequence." +pad = 0 + +[[variables.auxiliary]] +name = "tail" +type = "Bit" +desc = "Whether $#`count` < 8$, i.e. whether this row copies a single byte rather than eight." +pad = 1 + +[[variables.auxiliary]] +name = "value" +type = "DWordBL" +desc = "The bytes copied by this row; only $#`value`_0$ is copied when $#`tail` = 1$." +pad = 0 + +# Virtual + +[[variables.virtual]] +name = "step" +type = "Byte" +desc = "The number of bytes copied by this row: eight, or one when `tail` is set." +def = ["-", 8, ["*", 7, "tail"]] + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +# Assumptions + +[[assumptions]] +desc = "`IS_WORD[timestamp]`" +ref = "dma:a:timestamp" + +[[assumptions]] +desc = "`IS_WORD[src[i]]`" +iter = ["i", 0, 1] +ref = "dma:a:src" + +[[assumptions]] +desc = "`IS_WORD[dst[i]]`" +iter = ["i", 0, 1] +ref = "dma:a:dst" + +[[assumptions]] +desc = "`IS_WORD[count[i]]`" +iter = ["i", 0, 1] +ref = "dma:a:count" + +# Constraints + +[[constraint_groups]] +name = "incoming" + +[[constraints.incoming]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["cast", ["-", ["^", 2, 64], 3], "DWordWL"]] +multiplicity = ["-", "first"] +ref = "dma:c:receive_ecall" + +[[constraint_groups]] +name = "read_input" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [10, "dst", "timestamp"] +output = "dst" +cond = "first" +ref = "dma:c:read_dst" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [11, "src", "timestamp"] +output = "src" +cond = "first" +ref = "dma:c:read_src" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [12, "count", "timestamp"] +output = "count" +cond = "first" +ref = "dma:c:read_count" + +[[constraint_groups]] +name = "width" + +[[constraints.width]] +kind = "interaction" +tag = "ALU" +input = ["count", ["cast", 8, "DWordWL"], ["opsel", "LT"]] +output = ["arr", "tail", 0] +multiplicity = "μ" +ref = "dma:c:tail" + +[[constraints.width]] +kind = "interaction" +tag = "ALU" +input = ["count", ["cast", 257, "DWordWL"], ["opsel", "LT"]] +output = ["arr", 1, 0] +multiplicity = "first" +ref = "dma:c:bound" + +[[constraint_groups]] +name = "copy" + +[[constraints.copy]] +kind = "interaction" +tag = "MEMW" +input = [0, "src", "value", ["+", "timestamp", 1], 0, 0, ["not", "tail"]] +output = "value" +multiplicity = ["-", "μ", "end"] +ref = "dma:c:read_value" + +[[constraints.copy]] +kind = "interaction" +tag = "MEMW" +input = [0, "dst", "value", ["+", "timestamp", 2], 0, 0, ["not", "tail"]] +multiplicity = ["-", "μ", "end"] +ref = "dma:c:write_value" + +[[constraints.copy]] +kind = "arith" +constraint = "$#`tail` => #`value`_i = 0$" +poly = ["*", "tail", ["idx", "value", "i"]] +iter = ["i", 1, 7] +ref = "dma:c:tail_lanes" + +[[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 = "dma:c:src_incr" + +[[constraints.incr_decr]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "src_incr", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ" +ref = "dma:c:range_src_incr" + +[[constraints.incr_decr]] +kind = "template" +tag = "ADDNW" +input = ["dst", ["arr", "step", 0]] +output = ["cast", "dst_incr", "DWordWL"] +cond = ["-", "μ", "end"] +ref = "dma:c:dst_incr" + +[[constraints.incr_decr]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "dst_incr", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ" +ref = "dma:c:range_dst_incr" + +[[constraints.incr_decr]] +kind = "template" +tag = "SUB" +input = ["count", ["arr", "step", 0]] +output = ["cast", "count_decr", "DWordWL"] +ref = "dma:c:count_decr" + +[[constraints.incr_decr]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "count_decr", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ" +ref = "dma: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 = "dma:c:end" + +[[constraint_groups]] +name = "bits" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["first"] +ref = "dma:c:range_first" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["end"] +ref = "dma:c:range_end" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["tail"] +ref = "dma:c:range_tail" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["μ"] +ref = "dma:c:range_mu" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`first` + #`end` => #`μ` = 1$" +poly = ["*", ["+", "first", "end"], ["not", "μ"]] +ref = "dma:c:first_or_end_implies_mu" + +[[constraint_groups]] +name = "lookups" + +[[constraints.lookups]] +kind = "interaction" +tag = "DMA_NEXT" +input = ["timestamp", ["cast", "src_incr", "DWordWL"], ["cast", "dst_incr", "DWordWL"], ["cast", "count_decr", "DWordWL"]] +multiplicity = ["-", "μ", "end"] +ref = "dma:c:send_copy_next_chunk" + +[[constraints.lookups]] +kind = "interaction" +tag = "DMA_NEXT" +input = ["timestamp", "src", "dst", "count"] +multiplicity = ["-", ["-", "μ", "first"]] +ref = "dma:c:receive_copy_next_chunk" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index bdc85f9bf..99a4810ff 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -28,6 +28,14 @@ input = ["DWordWL", "DWordWL"] output = "DWordWL" cond = "BaseField" +# cond => ADDNW +[[signatures]] +tag = "ADDNW" +kind = "template" +input = ["DWordWL", "DWordWL"] +output = "DWordWL" +cond = "BaseField" + # cond => NEG [[signatures]] tag = "NEG" @@ -124,6 +132,12 @@ tag = "CNB" kind = "interaction" input = ["Word", "BaseField", "DWordWL", "DWordWL"] +# DMA_NEXT[timestamp, src, dst, count] +[[signatures]] +tag = "DMA_NEXT" +kind = "interaction" +input = ["Word", "DWordWL", "DWordWL", "DWordWL"] + # BYTE_ALU[res; selector, X, Y] [[signatures]] tag = "BYTE_ALU" From 1dd720b1201e1602efc21010633bb78fd928f3ec Mon Sep 17 00:00:00 2001 From: Nicole Date: Tue, 11 Aug 2026 16:49:02 -0300 Subject: [PATCH 2/4] Correct the padding, chunk-width and zero-length claims in the DMA chapter --- spec/dma.typ | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/spec/dma.typ b/spec/dma.typ index 652973310..f72e5a2b2 100644 --- a/spec/dma.typ +++ b/spec/dma.typ @@ -26,7 +26,7 @@ This accelerator replaces all of that with a single row per eight copied bytes. #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) -The #dma chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: +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 @@ -71,7 +71,7 @@ The guest-side `memcpy` chunks larger copies into multiple `ECALL`s; the executo #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 three 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. + 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 @@ -118,6 +118,7 @@ We use the `end` bit to indicate these circumstances. $ 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). @@ -141,8 +142,9 @@ 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: $#`tail` = 1$ makes $#`step` = 1$, which $#`count` = 1$ and $#`count_decr` = 0$ then satisfy. -The same holds for the two address updates, whence $#`src_incr` = #`dst_incr` = 1$. +@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. From dc0d71db2ac9695640e1811e0154288f1bb65c77 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 10:42:14 -0300 Subject: [PATCH 3/4] Match ADDNW to the implementation and correct the DMA chapter's termination, end-detection and row-count arguments --- spec/add.typ | 11 +++++---- spec/book.typ | 2 +- spec/dma.typ | 53 +++++++++++++++++++++++++++++++------------- spec/src/add_nw.toml | 8 +++---- spec/src/dma.toml | 7 +++--- 5 files changed, 51 insertions(+), 30 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index 386d52d2a..c220f42b3 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -10,8 +10,8 @@ #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 nw_interactions = compute_nr_interactions(nwchip) #let add = raw(chip.name) #let sub = raw(subchip.name) @@ -58,13 +58,16 @@ This template introduces the following constraints = #addnw -#add asserts an equality modulo $2^64$; #addnw is the variant that additionally rules out the wraparound. +#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 relation itself is delegated to #add; all #addnw adds is that the carry out of the most significant limb vanishes. +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 #nr_interactions interaction(s). +This template introduces #nw_interactions interaction(s). #render_chip_variable_table(nwchip, config) == Assumptions diff --git a/spec/book.typ b/spec/book.typ index 34a466fb0..54272cf0a 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -22,7 +22,7 @@ ("is_bit.typ", [`IS_BIT` template], ), ("is_byte.typ", [`IS_BYTE` template], ), ("sign.typ", [`SIGN` template], ), - ("add.typ", [`ADD`/`SUB` template], ), + ("add.typ", [`ADD`/`SUB`/`ADDNW` templates], ), ("neg.typ", [`NEG` template], ), ("reg.typ", [`REG`/`REGW` template], ), )), diff --git a/spec/dma.typ b/spec/dma.typ index f72e5a2b2..07e979c38 100644 --- a/spec/dma.typ +++ b/spec/dma.typ @@ -17,8 +17,8 @@ #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. +#footnote([Linux man-page on `memcpy`; man7.org. #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 doubleword 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 @@ -32,8 +32,13 @@ The #dma chip is comprised of #nr_variables variables that are expressed using # = 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). +The obligations on `src`, `dst` and `count` concern the _first_ row of a copy sequence only: +every subsequent row receives all three over the `DMA_NEXT` bus, whose sender range-checks them (@dma:c:range_src_incr, @dma:c:range_dst_incr and @dma:c:range_count_decr). +On the first row they are discharged by the register file, outside this chapter. + +`timestamp` is different: it is forwarded verbatim by @dma:c:send_copy_next_chunk and never range-checked here. +The first row's `timestamp` is pinned by @dma:c:receive_ecall to the `CPU`'s preprocessed timestamp column (@vars), and every later row inherits it through the bus. +That column also carries $#`timestamp` = 4 dot (i + 1)$, which is what keeps $#`timestamp` + 2$ from leaving the `Word` range in @dma:c:write_value --- `IS_WORD` alone would not. = Constraints In this VM, we assign system call number $-3$ to the #dma accelerator. @@ -65,7 +70,7 @@ A row copies eight bytes whenever at least eight bytes remain, and a single byte 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. +@dma:c:bound therefore proves $#`count` < 257$ on the first row of every sequence, which caps a sequence at $39$ rows --- attained at $n = 255$, not at $n = 256$, since a byte short of the bound trades one eight-byte row for seven one-byte rows. 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") @@ -86,19 +91,20 @@ A single `ECALL` hence behaves like `memmove` rather than like a byte-by-byte fo #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. +@dma:c:tail_lanes canonicalises a one-byte row. +Such a row addresses `MEMW` with $#`write2` = #`write4` = #`write8` = 0$, i.e. it presents a single-byte access. +`MEMW` gates every memory interaction for lane $i >= 1$ on those same width flags (@memw), so the seven unused lanes never reach the memory argument at all; +what they do reach is the `MEMW` tuple itself, and pinning them to zero is what keeps that tuple the canonical encoding of a single-byte access rather than one carrying seven free field elements. == 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. +The first two of @dma:c:range_src_incr, @dma:c:range_dst_incr and @dma: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") 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. + 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 --- and, less obviously, a sequence could close into a ring that balances every bus while copying nothing that was asked for; see the discussion of termination below. 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. @@ -116,7 +122,7 @@ We use the `end` bit to indicate these circumstances. $ 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. + Without those range checks the sum could _vanish_ for a `count_decr` other than $2^64 - 1$ --- one limb above $65535$ compensating another below it, as in $(65534, 65536, 65535, 65535)$ --- 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. @@ -130,7 +136,15 @@ without it, rows belonging to two different copies could be spliced into each ot 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. +It does not need one, but the reason is worth stating carefully, because the obvious counting argument is not sufficient on its own. + +Fix a timestamp. Balancing `DMA_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and @dma:c:receive_ecall caps the latter at one, since the `CPU` sends a single `ECALL` per timestamp. +So a sequence that simply runs on without ever setting `end` sends one tuple more than it receives, and the bus does not balance. + +That argument rules out an _open_ sequence, and nothing more. +It does not by itself rule out a _closed_ one: a ring of rows carrying $#`μ` = 1$ with neither `first` nor `end` set sends and receives one tuple each, so it balances, consumes no `ECALL` at all, and would still emit a read and a write per row. +What forbids the ring is @dma:c:src_incr: `ADDNW` forces $#`src_incr` = #`src` + #`step`$ _over the integers_ with $#`step` >= 1$, so `src` strictly increases along the chain and can never return to a value it already held. +This is the second reason the addresses use `ADDNW` rather than `ADD`, and the more important of the two. == 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). @@ -143,16 +157,23 @@ To pad this chip, use the below data. 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. +The two address updates are conditioned on $#`μ` - #`end`$ and so do not forbid a wraparound here, but their low-limb carry is constrained on every row (@addnw:c:carry), which forces $#`src_incr` = #`dst_incr` = 1$. +A padding row is therefore an inactive one-byte step rather than an arbitrary row. = 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. + On a row that copies, 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. + On a row that copies nothing --- the terminal row, and padding rows --- there is no read, so $#`value`_0$ is an arbitrary field element there. + That is harmless, because @dma:c:write_value carries the same multiplicity and so does not fire either. +- @dma:c:range_src_incr and @dma:c:range_dst_incr carry multiplicity $#`μ`$, but `src_incr` and `dst_incr` are constrained and consumed only at $#`μ` - #`end`$. + Lowering both to $#`μ` - #`end`$ would drop eight `IS_HALF` lookups on every terminal row at no cost. + @dma:c:range_count_decr genuinely needs $#`μ`$, since @dma:c:end consumes `count_decr` at that multiplicity. - `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. + For a copy of exactly $256$ bytes the row count would drop from $33$ to $17$ and $9$. + The _worst case_ over all admissible lengths behaves quite differently, however, since it is attained at $n = 255$ rather than at $n = 256$: it is $31 + 7 + 1 = 39$ rows today, $15 + 15 + 1 = 31$ with sixteen-byte rows, and $7 + 31 + 1 = 39$ again with thirty-two-byte rows. + Widening the chunk moves work out of the wide rows and into the one-byte tail, so past sixteen bytes it buys nothing at all where it matters. diff --git a/spec/src/add_nw.toml b/spec/src/add_nw.toml index ef86adeec..407767f12 100644 --- a/spec/src/add_nw.toml +++ b/spec/src/add_nw.toml @@ -55,11 +55,9 @@ name = "all" [[constraints.all]] kind = "template" -tag = "ADD" -input = ["lhs", "rhs"] -output = "sum" -cond = "cond" -ref = "addnw:c:add" +tag = "IS_BIT" +input = [["idx", "carry", 0]] +ref = "addnw:c:carry" [[constraints.all]] kind = "arith" diff --git a/spec/src/dma.toml b/spec/src/dma.toml index 7ddf2c52d..34c587287 100644 --- a/spec/src/dma.toml +++ b/spec/src/dma.toml @@ -1,5 +1,4 @@ name = "DMA" -code = "DMA" # Input @@ -68,7 +67,7 @@ pad = 1 [[variables.auxiliary]] name = "value" type = "DWordBL" -desc = "The bytes copied by this row; only $#`value`_0$ is copied when $#`tail` = 1$." +desc = "The bytes copied by this row; only $#`value`_0$ is copied when $#`tail` = 1$. Unconstrained on rows that copy nothing." pad = 0 # Virtual @@ -76,7 +75,7 @@ pad = 0 [[variables.virtual]] name = "step" type = "Byte" -desc = "The number of bytes copied by this row: eight, or one when `tail` is set." +desc = "The stride this row advances by: eight, or one when `tail` is set. No bytes are copied on the terminal row." def = ["-", 8, ["*", 7, "tail"]] # Multiplicity @@ -116,7 +115,7 @@ name = "incoming" [[constraints.incoming]] kind = "interaction" tag = "ECALL" -input = ["timestamp", ["cast", ["-", ["^", 2, 64], 3], "DWordWL"]] +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 3], ["-", ["^", 2, 32], 1]]] multiplicity = ["-", "first"] ref = "dma:c:receive_ecall" From 6a16bfc6cc44f358bfccf2dade27728e89f66406 Mon Sep 17 00:00:00 2001 From: Nicole Date: Wed, 12 Aug 2026 16:09:08 -0300 Subject: [PATCH 4/4] Say that the padding row's low-limb carry permits rather than forces the unit address increments --- spec/dma.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/dma.typ b/spec/dma.typ index 07e979c38..40ff30abe 100644 --- a/spec/dma.typ +++ b/spec/dma.typ @@ -157,8 +157,8 @@ To pad this chip, use the below data. 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 are conditioned on $#`μ` - #`end`$ and so do not forbid a wraparound here, but their low-limb carry is constrained on every row (@addnw:c:carry), which forces $#`src_incr` = #`dst_incr` = 1$. -A padding row is therefore an inactive one-byte step rather than an arbitrary row. +The two address updates are conditioned on $#`μ` - #`end`$ and so do not forbid a wraparound here, but their low-limb carry is constrained on every row (@addnw:c:carry), so a padding row must satisfy that relation too; $#`src_incr` = #`dst_incr` = 1$ is the assignment that does so with a zero carry. +It is not the only one --- @dma:c:range_src_incr and @dma:c:range_dst_incr, which would pin the limbs, carry multiplicity $#`μ`$ and are inert here --- but a padding row feeds no interaction either way. = 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.