From d26613495db81940c3d7a9eb7d71c315fa682131 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 11 Sep 2026 09:27:43 -0300 Subject: [PATCH 1/4] Specify the unified MEMMOVE accelerator --- spec/chapters/about_ecalls.typ | 5 + spec/chapters/add.typ | 27 ++ spec/chapters/commit.typ | 86 ++----- spec/chapters/memmove.typ | 290 +++++++++++++++++++++ spec/meta.typ | 3 +- spec/src/add_nw.toml | 66 +++++ spec/src/commit.toml | 148 +---------- spec/src/memmove.toml | 454 +++++++++++++++++++++++++++++++++ spec/src/signatures.toml | 20 +- 9 files changed, 893 insertions(+), 206 deletions(-) create mode 100644 spec/chapters/memmove.typ create mode 100644 spec/src/add_nw.toml create mode 100644 spec/src/memmove.toml diff --git a/spec/chapters/about_ecalls.typ b/spec/chapters/about_ecalls.typ index 102d7a504..173ac14c1 100644 --- a/spec/chapters/about_ecalls.typ +++ b/spec/chapters/about_ecalls.typ @@ -35,3 +35,8 @@ 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` +/ -32: `MEMMOVE`/`memset` (@memmove) + +The `HINT` `ECALL` is allocated but not yet specified; the number is listed so that it is not handed out twice. diff --git a/spec/chapters/add.typ b/spec/chapters/add.typ index a3e64f493..2482e402f 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. + +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$. diff --git a/spec/chapters/commit.typ b/spec/chapters/commit.typ index 14aa1dedc..01d7a0d31 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,6 +12,9 @@ #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) @@ -26,10 +27,6 @@ The #commit chip leverages #nr_variables variables, spanning #nr_columns columns 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) +Since every constraint in this chip is conditioned on `μ`, 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..0a8b5ab50 --- /dev/null +++ b/spec/chapters/memmove.typ @@ -0,0 +1,290 @@ +#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 single copying primitive of this VM: one chip serves `memcpy`, `memmove`, `memset` and the byte loop of a commitment. +#footnote([Linux man-pages on `memmove`, `memcpy` and `memset`; man7.org. #link("https://man7.org/linux/man-pages/man3/memmove.3.html")[[src]]]) +Without it the guest would run these loops in RISC-V --- per doubleword a load, a store, two pointer increments and a branch, five instructions the proof pays for. + +The three functionalities differ only in where the bytes go and in which of the two accesses happens first: + +#figure( + table( + columns: 5, + align: left, + table.header[*functionality*][*entered by*][*destination*][*read at*][*write at*], + [`memcpy`/`memmove`], [`ECALL` $-30$], [RAM], [$#`timestamp` + 1$], [$#`timestamp` + 2$], + [`memset`], [`ECALL` $-32$], [RAM], [$#`timestamp` + 2$], [$#`timestamp` + 1$], + [`commit`], [`COMMIT` (@commit)], [commitment domain], [$#`timestamp` + 1$], [---], + ), + caption: [The three functionalities of #memmove.], +) + +Neither the destination domain nor the order of the two accesses is chosen by the caller. +Both are derived from `is_set` and `is_commit`, and those two bits are in turn 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 interactions: +#render_chip_variable_table(chip, config) + += Assumptions +#render_chip_assumptions(chip, config) + +These assumptions concern the _first_ row of a sequence. +There, `src`, `dst` and `count` come either from the register file or from `COMMIT`, and `timestamp` from the `CPU`. +Every later row receives all four over the `MEMMOVE_NEXT` bus, where @memmove:c:range_src_incr, @memmove:c:range_dst_incr and @memmove:c:range_count_decr range-check three of them on the sending side. +The fourth, `timestamp`, is range-checked by neither side; it holds because the value travels unchanged from the `ECALL` at the root of the sequence, which is where @memmove:a:timestamp is discharged. + +@memmove:a:dst is the one that is not discharged on a commitment sequence: `dst` is then an index rather than an address, and `COMMIT` carries it as a `BaseField`. +Nothing here leans on it. +The gap of @memmove:c:set_gap_lo is read over the integers only for `memset`, which is not a commitment, and the strict increase that rules out a ring below is a statement about `src`, which `COMMIT` does read from `x11`. +A denormalized index reaches no chip other than this one, and the memory argument stays consistent for it as it does for any other address. + += Constraints +This VM assigns system call number $-30$ to the copy functionality 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. +A sequence is therefore entered exactly once, and only that first row accepts an entry. +There are two ways in: from the `CPU`, by accepting an `ECALL`, or from `COMMIT`, which keeps the `write` system call for itself and defers only the byte loop. +#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`$, a linear function of the selector, so `is_set` is decoded from the `ECALL` the guest actually executed rather than chosen by the prover. +`is_commit` is decoded from _which_ bus the first row accepted from: `COMMIT_DEFER` has exactly one sender, and that is `COMMIT`. + +#aside("The syscall number alone does not pin the selector")[ + As a line in `is_set`, the expression in @memmove:c:receive_ecall runs over the whole field, so for _every_ system call number there is a field element that reproduces its tuple. + @memmove:c:range_is_set is what rules those out, and it therefore carries the whole decoding argument. + This matters when `ECALL` numbers are allocated (@ecall): a number is safe from this chip because `is_set` is a bit, never because it is far away from $-30$ and $-32$. +] + +@memmove:c:one_hot makes the two selectors mutually exclusive and @memmove:c:functionality_implies_mu keeps both clear on a padding row. +Both selectors also ride _inside_ the `MEMMOVE_NEXT` tuple in either direction (@memmove:c:send_next_chunk, @memmove:c:receive_next_chunk), so a sequence cannot change functionality half way through it. +#render_constraint_table(chip, config, groups: "functionality") + +The last three of these define nothing new; they are the two selectors combined with `first` and with $#`μ` - #`end`$. +They exist as columns because a multiplicity has to be linear in the columns of the chip (@logup), and a product of two of them is not. +The remaining combinations, `first_defer` and `ram_write`, are differences of columns and so need no column of their own. + +== Reading the operands +The guest-side `memcpy` this chip accelerates 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`; the number of bytes to move. + +`memset` uses the same three registers for the same three roles --- `A1` is a source address there too, not a fill byte --- and what the guest puts in them is discussed at the bottom of this chapter. +@memmove:c:read_dst, @memmove:c:read_src and @memmove:c:read_count read the three registers. +Each of them writes back the value that was read, so the operation leaves the registers untouched; +the guest is responsible for producing the return value. +These reads are conditioned on `first_ecall`: a deferred commitment sequence takes its operands from `COMMIT` instead, which has already read the registers of the `write` system call. +#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 $#`short` = (#`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 left free: the prover may cut any row down to a single byte. +That freedom is what lets a schedule walk one-byte rows until both ends are eight-aligned and then take wide rows through the body, which is the condition under which those rows are admitted by `MEMW_A` rather than by the wider `MEMW` (@memw). +Which schedule is used is a prover-side choice; the AIR grants the freedom and charges for the rows. + +Because a row is the unit in which this chip charges, an unbounded `count` would let a single guest instruction append an unbounded number of rows to the trace. +@memmove:c:bound therefore proves $#`count` < 257$ on the first row of every `ECALL`-entered sequence, which caps it at $257$ rows --- the bound is the one-byte-per-row schedule, not the honest one. +The guest-side stubs chunk larger operations into multiple `ECALL`s; the executor rejects any chunk exceeding 256 bytes. +#render_constraint_table(chip, config, groups: "width") + +Note that @memmove:c:bound carries `first_ecall`, so a commitment sequence proves no byte bound at all --- and `COMMIT` range-checks no `count` either. +This is a bound on prover cost and nothing else: the commitment bus still has to balance against the committed output, which the verifier knows in full, so a commitment sequence can only be as long as the output it produces. + +#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 move +The bytes are read at $#`timestamp` + 1 + #`is_set`$ and written at $#`timestamp` + 2 - #`is_set`$: the two accesses are one timestamp apart, and `is_set` decides which of them comes first. +The `CPU`'s preprocessed timestamp column holds $4 dot (i + 1)$ at row $i$ (@vars), so neither expression can leave the `Word` range --- `IS_WORD` on `timestamp` alone would not rule that out. +Both interactions are expressed over the _same_ `value` variable, which is what makes the moved 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`. +#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. +With the normal order that makes every read observe memory as it was before the sequence started, which is precisely `memmove`'s guarantee for an overlapping range. +With the order inverted every read instead observes memory after all of the sequence's writes, and the sequence propagates rather than copies; that is `memset`, and @memmove:c:set_gap_lo and @memmove:c:set_gap_hi are what make it well-defined. +Both orders keep the read and the write at distinct timestamps and both strictly after `timestamp`, so the memory argument is undisturbed either way. + +@memmove: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. + +Which memory chip the two accesses reach is decided by their addresses, and this chip constrains neither. +An eight-byte access lands on `MEMW_A`, the read-size aligned fast path (@memw), when its address is eight-byte aligned and all eight bytes were last touched at one timestamp: that chip stores a single old timestamp, so it needs one `LT` row (@lt) to order the access. +Anything else falls to the general `MEMW`, which stores one old timestamp per byte and needs eight, on a row that is the wider of the two to begin with. +The read and the write are routed independently, so a sequence can take the fast path at one end and not at the other, and --- since the width of a row is not tied to `count` --- a schedule is free to spend one-byte rows up front to bring an end into alignment. +A misaligned sequence therefore commits more cells than an aligned one of the same length, which is why the row counts this chapter reasons about are not on their own the cost of an operation. + +== Writing to the commitment domain +When `is_commit` is set the destination is not RAM. +`dst` is then the index of the byte in the committed output rather than an address#footnote[ + For very large commitments (with index $>= 2^32$), the commitment-domain address can become denormalized, but since no other chip interacts with this memory domain, there is no issue. + The usual consistency guarantee from the LogUp argument and correct initialization as for general addresses applies. +], and the write goes to a domain-separated part of memory with domain 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 therefore gated on `ram_write` and does not fire, and @memmove:c:commit_value_out and @memmove:c:commit_value_in take its place. +These need no `MEMW`: a commitment cell is written once and read by nobody, so there is no old value to produce and no timestamp to order. +#render_constraint_table(chip, config, groups: "commit") + +A committing row emits one interaction _per byte_, at index $#`dst` + i$, rather than one for the row. +The grouping is what forces that. +The verifier reconstructs this side of the bus from the committed output alone, and what it sees there is the concatenation of every commitment the program made --- not where one `write` ended and the next began. +It therefore cannot reproduce the prover's row schedule, which restarts at every system call: a guest committing four bytes and then four more sends eight one-byte rows where a verifier chunking the eight bytes it sees would expect a single wide row, and an honest proof would be rejected. +Addressing every byte by its own index leaves the two sides nothing to disagree about. +`commit_lane` is what keeps a one-byte 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 that still have to be moved afterwards. +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") + +Note the asymmetry between the two position updates and the count update: + ++ 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 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 moving 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 @memmove:c:send_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 because $#`step` <= #`count`$ on every row with $#`count` >= 1$: a wide row needs $#`short` = 0$ by @memmove:c:wide_needs_eight and hence $#`count` >= 8 = #`step`$, and a narrow row has $#`step` = 1$. + The subtraction can therefore only wrap on the terminal row. + +== 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 `COMMIT` used to (@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 @memmove: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 _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 the read and both writes carry a multiplicity that vanishes with `end`, a row that wrongly claims `end` emits no memory operations at all, which is a silently truncated operation with every bus balanced. ++ $#`end` = 1$ still forces $#`count` = 0$ even though the prover picks the width. + The other candidate is $#`count` = 7$ with a wide row, which wraps `count_decr` to $2^64 - 1$; but $#`count` = 7$ gives $#`short` = 1$, and @memmove:c:wide_needs_eight then rejects the wide row. ++ An operation on zero bytes is a single row with $#`first` = #`end` = 1$: it accepts the entry 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 move the next chunk over the `MEMMOVE_NEXT` bus, specifying the timestamp, the positions to continue reading and writing at, the number of bytes that still have to be moved, and the functionality (@memmove:c:send_next_chunk). +Since that certainly won't be the `first` row of the sequence, we read `src_incr`, `dst_incr` and `count_decr` from the previous recursion level into `src`, `dst` and `count`, and continue. +#render_constraint_table(chip, config, groups: "lookups") + +Both tuples carry the `timestamp`, and that is what separates one sequence from another: +without it, rows belonging to two different sequences could be spliced into each other's while the bus still balances. +Since the CPU's timestamps strictly increase per instruction, no two #memmove sequences share one. + +Observe also that this chip has no constraint demanding that a sequence terminates. +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 `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ caps the latter at one. +The `CPU` sends a single `ECALL` per timestamp, which is what caps @memmove:c:receive_ecall; and `COMMIT` puts at most one row on `COMMIT_DEFER` per timestamp, for the same reason, which is what caps @memmove:c:receive_commit_defer. +The two are moreover exclusive, since that single `ECALL` cannot be both a copy and a `write`. +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 entry at all, and would still emit a read and a write per row. +What forbids the ring is @memmove:c:src_incr: `ADDNW` forces $#`src_incr` = #`src` + #`step`$ _over the integers_ with $#`step` >= 1$, so `src` strictly increases along the sequence and can never return to a value it already held. +This is the second reason the positions use `ADDNW` rather than `ADD`, and the more important of the two. + +== Bits +Lastly, we must make sure the seven independent bits are bits, and that either $#`first` = 1$ or $#`end` = 1$ implies $#`μ` = 1$ (@memmove:c:first_or_end_implies_mu). +The latter is required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary. +`first_ecall`, `commit_write` and `commit_write_wide` need no range check of their own: the constraints of @memmove:c:first_ecall, @memmove:c:commit_write and @memmove:c:commit_write_wide already equate each of them to a product of bits. +#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. +@memmove: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. +$#`tail` = 1$ in turn satisfies @memmove:c:wide_needs_eight for either value of `short`. +The two position 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. + += `memset` as a propagating `memmove` +`memset` needs no machinery of its own beyond the inverted order, but it does need the guest to hand it the right operands. + +The stub seeds the first eight bytes of the range with ordinary stores and then calls the accelerator with `src` the start of that seed, `dst` its end and `count` the remaining length; fills shorter than sixteen bytes take a plain store loop instead, since they cannot amortise the seed. +The row at offset $k$ then reads at $#`src` + k$ and writes at $#`src` + k + 8$. +Because every row of the sequence writes at $#`timestamp` + 1$ and reads at $#`timestamp` + 2$, each read observes the whole sequence's writes, so the row forces $"mem"[#`src` + k + 8] = "mem"[#`src` + k]$ for every $k$, and the eight seeded bytes are replicated across the range. +The recursion bottoms out in the seed, which the sequence never wrote. +None of this depends on how the prover schedules the widths. + +@memmove:c:set_gap_lo and @memmove:c:set_gap_hi pin the gap, and the pinning is load-bearing rather than a convention. +The degenerate case is $#`dst` = #`src`$: the read and the write then address the same cell at two adjacent timestamps, the memory argument is satisfied by $#`value` = #`value`$, and all eight lanes become free field elements. +Nothing else in this chip touches them --- they are typed as bytes but range-checked nowhere, because on a moving row @memmove:c:read_value pins them --- so a prover could put anything it liked into RAM, and hence into the committed output. + +Three details of the pinning are worth spelling out: +- The distance must be at least the width of the widest row, so $8$ is the smallest one that works. + At distance $1$ an eight-byte row's read range overlaps its own write range and the argument above returns. +- The gate is `is_set` alone, and not `is_set` together with a multiplicity. + `step` advances `src` and `dst` together, so $#`dst` - #`src`$ is invariant along a sequence and the relation holds on the terminal row as well; a padding row leaves $#`is_set` = 0$. + Gating on a product would cost a degree, and this chip stays at degree 2. +- Taken together the two constraints force $#`dst` - #`src` = 8$ _in the field_, whichever way the prover splits the two addresses over their limbs, and that is already enough to rule out the aliasing. + Reading them as a gap of $8$ over the integers additionally needs @memmove:a:src and @memmove:a:dst, which the register file discharges on the first row and @memmove:c:range_src_incr and @memmove:c:range_dst_incr on every later one. + += 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. #link("https://github.com/eth-act/zkevm-standards/tree/main/standards/accelerated-memory-operations")[[src]]]) + +Two of its requirements fall outside this chapter. +The first is behavioural: the accelerated symbol must behave identically to the C library function, which the guest-side stub is responsible for. +The second concerns linking: the symbol must be a strong definition in an unconditionally linked object, or be linked with `--whole-archive`, so that a weak definition elsewhere cannot silently displace it. + +What the standard asks of the chip itself is that it accept operands of arbitrary alignment, which it does: no constraint here refers to the alignment of `src`, `dst` or `count`, and a row's width is not tied to any of them. +The standard's fourth operation, `memcmp`, is not covered: it does not copy, so it does not fit this chip, and accelerating it would need a table of its own. + += Notes/optimizations +- `COMMIT` could send its deferral on `MEMMOVE_NEXT` directly, with $#`is_commit` = 1$ in the tuple, which would retire the `COMMIT_DEFER` bus and the `first_ecall` column. + A commitment sequence would then have no `first` row at all, so `first` would come to mean "entered by `ECALL`" rather than "head of the sequence", and $#`first` dot #`is_commit` = 0$ would have to be added to stop an `ECALL`-entered sequence from writing to the commitment domain. +- `count` need not be a full `DWordWL` on the `ECALL` path: @memmove:c:bound already proves $#`count` < 257$ there, and every later `count` is smaller still. + The commitment path has no such bound, so this would have to be paid for with a range check where the value enters from `COMMIT`. +- The `value` variable is typed as bytes, but this chip range-checks none of its lanes. + On a row that moves, they are pinned by @memmove: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 @memmove:c:tail_lanes, since those never reach the read. + On a row that moves nothing --- the terminal row, and padding rows --- there is no read, so $#`value`_0$ is an arbitrary field element there. + That is harmless, because every write carries a multiplicity that vanishes with `end` and so does not fire either. +- @memmove:c:range_src_incr and @memmove: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. + It would not make the proof smaller, though: `IS_HALF` is answered by a preprocessed table whose height is fixed at compile time, so dropping lookups moves multiplicities and leaves the number of committed cells where it was. + @memmove:c:range_count_decr genuinely needs $#`μ`$, since @memmove:c:end consumes `count_decr` at that multiplicity. +- A row could move sixteen or thirty-two bytes rather than eight, at the cost of a wider `MEMW` signature. + It would also narrow the aligned fast path: `MEMW_A` admits an access only when it is aligned to its own width, so sixteen-byte rows would need sixteen-byte-aligned ends to stay on the cheap chip, and the widths `MEMW`'s signature can express today are one, two, four and eight. + Rows saved and cells saved therefore move in opposite directions here, and only the second is what the proof pays for. +- The `memmove` property belongs to one `ECALL`, not to an arbitrarily large guest-level copy: a copy larger than 256 bytes is split by the guest stub into several `ECALL`s at distinct timestamps, and chunk $k+1$ reads what chunk $k$ has already written. + That is in-contract for `memcpy`, whose buffers may not overlap; a guest-side `memmove` has to keep each copy within a single `ECALL`, or chunk in the direction that preserves the semantics. diff --git a/spec/meta.typ b/spec/meta.typ index fc6bc783b..dada8202d 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -19,7 +19,7 @@ ("is_bit", [`IS_BIT` template], ), ("is_byte", [`IS_BYTE` template], ), ("sign", [`SIGN` template], ), - ("add", [`ADD`/`SUB` template], ), + ("add", [`ADD`/`SUB`/`ADDNW` templates], ), ("neg", [`NEG` template], ), ("reg", [`REG`/`REGW` template], ), )), @@ -49,6 +49,7 @@ ("commit", [`COMMIT` chip], ), ("sha256", [`SHA256` accelerator], ), ("keccak", [`KECCAK` accelerator], ), + ("memmove", [`MEMMOVE` accelerator], ), ("ecsm", [`ECSM` accelerator], ), ("fext", [Extension field accelerator], ), )), 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..d9caa9d21 100644 --- a/spec/src/commit.toml +++ b/spec/src/commit.toml @@ -12,7 +12,7 @@ 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]] @@ -21,40 +21,10 @@ type = "DWordWL" 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..e759fc4d1 --- /dev/null +++ b/spec/src/memmove.toml @@ -0,0 +1,454 @@ +name = "MEMMOVE" + +# 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 = "short" +type = "Bit" +desc = "Whether $#`count` < 8$, i.e. whether eight bytes are still available to move." +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. No bytes are moved on the terminal row." +def = ["-", 8, ["*", 7, "tail"]] + +[[variables.virtual]] +name = "first_defer" +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_defer"] +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", "short", 0] +multiplicity = "μ" +ref = "memmove:c:short" + +[[constraints.width]] +kind = "arith" +constraint = "$#`short` => #`tail` = 1$" +poly = ["*", ["not", "tail"], "short"] +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 = ["short"] +ref = "memmove:c:range_short" + +[[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 +[[signatures]] +tag = "ADDNW" +kind = "template" +input = ["DWordWL", "DWordWL"] +output = "DWordWL" +cond = "BaseField" + # cond => NEG [[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]] From 250c654a6212e9de5de81c8cc08a709fcea8f58c Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 11 Sep 2026 10:27:00 -0300 Subject: [PATCH 2/4] Correct the MEMW_A admission condition and the memset limb-boundary contract --- spec/chapters/about_ecalls.typ | 4 +- spec/chapters/add.typ | 10 ++-- spec/chapters/commit.typ | 4 +- spec/chapters/memmove.typ | 98 ++++++++++++++++++---------------- spec/meta.typ | 2 +- spec/src/memmove.toml | 5 +- 6 files changed, 64 insertions(+), 59 deletions(-) diff --git a/spec/chapters/about_ecalls.typ b/spec/chapters/about_ecalls.typ index 173ac14c1..e2f6e0b2c 100644 --- a/spec/chapters/about_ecalls.typ +++ b/spec/chapters/about_ecalls.typ @@ -36,7 +36,5 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / -21: `FEXT_FMA` (@fext) / -22: `FEXT_ZERO` (@fext) / -30: `MEMMOVE`/`memcpy`/`memmove` (@memmove) -/ -31: `HINT` +/ -31: `HINT` (reserved, not yet specified) / -32: `MEMMOVE`/`memset` (@memmove) - -The `HINT` `ECALL` is allocated but not yet specified; the number is listed so that it is not handed out twice. diff --git a/spec/chapters/add.typ b/spec/chapters/add.typ index 2482e402f..0c1288c03 100644 --- a/spec/chapters/add.typ +++ b/spec/chapters/add.typ @@ -59,11 +59,6 @@ This template introduces the following constraints #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) @@ -77,3 +72,8 @@ This template introduces the following constraints 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 01d7a0d31..ffe7230ef 100644 --- a/spec/chapters/commit.typ +++ b/spec/chapters/commit.typ @@ -20,7 +20,7 @@ It is one row per system call; the loop over the buffer lives in the other 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 @@ -71,7 +71,7 @@ Lastly, we must make sure `μ` is a bit. To pad this chip, use the below data. #render_chip_padding_table(chip, config) -Since every constraint in this chip is conditioned on `μ`, a padding row is all-zero. +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`. diff --git a/spec/chapters/memmove.typ b/spec/chapters/memmove.typ index 0a8b5ab50..e5aa62844 100644 --- a/spec/chapters/memmove.typ +++ b/spec/chapters/memmove.typ @@ -41,7 +41,7 @@ Both are derived from `is_set` and `is_commit`, and those two bits are in turn d #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 interactions: +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 @@ -52,10 +52,7 @@ There, `src`, `dst` and `count` come either from the register file or from `COMM Every later row receives all four over the `MEMMOVE_NEXT` bus, where @memmove:c:range_src_incr, @memmove:c:range_dst_incr and @memmove:c:range_count_decr range-check three of them on the sending side. The fourth, `timestamp`, is range-checked by neither side; it holds because the value travels unchanged from the `ECALL` at the root of the sequence, which is where @memmove:a:timestamp is discharged. -@memmove:a:dst is the one that is not discharged on a commitment sequence: `dst` is then an index rather than an address, and `COMMIT` carries it as a `BaseField`. -Nothing here leans on it. -The gap of @memmove:c:set_gap_lo is read over the integers only for `memset`, which is not a commitment, and the strict increase that rules out a ring below is a statement about `src`, which `COMMIT` does read from `x11`. -A denormalized index reaches no chip other than this one, and the memory argument stays consistent for it as it does for any other address. +@memmove:a:dst is not discharged on a commitment sequence; that case is taken up at the end of this chapter. = Constraints This VM assigns system call number $-30$ to the copy functionality and $-32$ to `memset`. @@ -69,16 +66,16 @@ There are two ways in: from the `CPU`, by accepting an `ECALL`, or from `COMMIT` `is_commit` is decoded from _which_ bus the first row accepted from: `COMMIT_DEFER` has exactly one sender, and that is `COMMIT`. #aside("The syscall number alone does not pin the selector")[ - As a line in `is_set`, the expression in @memmove:c:receive_ecall runs over the whole field, so for _every_ system call number there is a field element that reproduces its tuple. - @memmove:c:range_is_set is what rules those out, and it therefore carries the whole decoding argument. - This matters when `ECALL` numbers are allocated (@ecall): a number is safe from this chip because `is_set` is a bit, never because it is far away from $-30$ and $-32$. + The low limb of @memmove:c:receive_ecall is a line in `is_set` and so runs over the whole field, while the high limb is the constant $2^32 - 1$. + Every system call number in the negative range is therefore reproduced by some field element, and @memmove:c:range_is_set is what rules those out --- it carries the whole decoding argument. + This matters when `ECALL` numbers are allocated (@ecall): a negative number is safe from this chip because `is_set` is a bit, never because it is far away from $-30$ and $-32$. ] @memmove:c:one_hot makes the two selectors mutually exclusive and @memmove:c:functionality_implies_mu keeps both clear on a padding row. Both selectors also ride _inside_ the `MEMMOVE_NEXT` tuple in either direction (@memmove:c:send_next_chunk, @memmove:c:receive_next_chunk), so a sequence cannot change functionality half way through it. #render_constraint_table(chip, config, groups: "functionality") -The last three of these define nothing new; they are the two selectors combined with `first` and with $#`μ` - #`end`$. +The last three of these define nothing new; they combine a selector with `first`, with $#`μ` - #`end`$, and with `tail` respectively. They exist as columns because a multiplicity has to be linear in the columns of the chip (@logup), and a product of two of them is not. The remaining combinations, `first_defer` and `ram_write`, are differences of columns and so need no column of their own. @@ -86,7 +83,7 @@ The remaining combinations, `first_defer` and `ram_write`, are differences of co The guest-side `memcpy` this chip accelerates has the following signature: ```c -void *memcpy(void dest[restrict count], const void src[restrict count], size_t count); +void *memcpy(size_t count; void dest[restrict count], const void src[restrict count], size_t count); ``` That is to say, @@ -105,7 +102,7 @@ These reads are conditioned on `first_ecall`: a deferred commitment sequence tak A row moves eight bytes, or a single byte when `tail` is set. @memmove:c:short pins $#`short` = (#`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 left free: the prover may cut any row down to a single byte. -That freedom is what lets a schedule walk one-byte rows until both ends are eight-aligned and then take wide rows through the body, which is the condition under which those rows are admitted by `MEMW_A` rather than by the wider `MEMW` (@memw). +That freedom is what lets a schedule choose where its wide rows fall, which is what decides whether they are admitted by `MEMW_A` rather than by the wider `MEMW` (@memw). Which schedule is used is a prover-side choice; the AIR grants the freedom and charges for the rows. Because a row is the unit in which this chip charges, an unbounded `count` would let a single guest instruction append an unbounded number of rows to the trace. @@ -114,11 +111,12 @@ The guest-side stubs chunk larger operations into multiple `ECALL`s; the executo #render_constraint_table(chip, config, groups: "width") Note that @memmove:c:bound carries `first_ecall`, so a commitment sequence proves no byte bound at all --- and `COMMIT` range-checks no `count` either. -This is a bound on prover cost and nothing else: the commitment bus still has to balance against the committed output, which the verifier knows in full, so a commitment sequence can only be as long as the output it produces. +No prover gain follows: the commitment bus still has to balance against the committed output, which the verifier knows in full, so a sequence can only be as long as the output it produces. +What it does cost is work, and not only the prover's --- the verifier contributes a token pair per committed byte --- so a `write` with an absurd `count` is unprovable and unverifiable rather than merely expensive. #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. + Splitting the remainder into four-, two- and one-byte chunks instead would shave off at most eight 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 move @@ -134,16 +132,15 @@ With the normal order that makes every read observe memory as it was before the With the order inverted every read instead observes memory after all of the sequence's writes, and the sequence propagates rather than copies; that is `memset`, and @memmove:c:set_gap_lo and @memmove:c:set_gap_hi are what make it well-defined. Both orders keep the read and the write at distinct timestamps and both strictly after `timestamp`, so the memory argument is undisturbed either way. -@memmove: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. +@memmove:c:tail_lanes canonicalises a one-byte row, which addresses `MEMW` with $#`write2` = #`write4` = #`write8` = 0$. +`MEMW` gates lane $i >= 1$ on those same flags (@memw), so the seven unused lanes never reach the memory argument --- but they do reach the `MEMW` tuple, and pinning them to zero is what keeps it the canonical encoding of a single-byte access rather than one carrying seven free field elements. Which memory chip the two accesses reach is decided by their addresses, and this chip constrains neither. -An eight-byte access lands on `MEMW_A`, the read-size aligned fast path (@memw), when its address is eight-byte aligned and all eight bytes were last touched at one timestamp: that chip stores a single old timestamp, so it needs one `LT` row (@lt) to order the access. -Anything else falls to the general `MEMW`, which stores one old timestamp per byte and needs eight, on a row that is the wider of the two to begin with. -The read and the write are routed independently, so a sequence can take the fast path at one end and not at the other, and --- since the width of a row is not tied to `count` --- a schedule is free to spend one-byte rows up front to bring an end into alignment. -A misaligned sequence therefore commits more cells than an aligned one of the same length, which is why the row counts this chapter reasons about are not on their own the cost of an operation. +`MEMW_A` is the fast path (@memw): it stores a single old timestamp, so it needs one `LT` row (@lt) to order the access, where the general `MEMW` stores one per byte and needs eight, on a row that is the wider of the two to begin with. +Two conditions admit an access there, and neither is the eight-byte alignment of its address: the access must not cross a $2^16$ limb boundary, and all the bytes it touches must carry the same old timestamp. +Alignment matters only through the second: a buffer last written in eight-byte aligned groups has one timestamp per group, so an eight-byte access that sits on a group reads one timestamp and an access that straddles two reads two. +That is what a schedule is buying when it spends one-byte rows to move a wide row onto a group boundary, and it is a property of how the buffer was written rather than of this chip. +The read and the write are routed independently, so a sequence can take the fast path at one end and not at the other, and the row counts this chapter reasons about are therefore not on their own the cost of an operation. == Writing to the commitment domain When `is_commit` is set the destination is not RAM. @@ -159,12 +156,10 @@ When `is_commit` is set the destination is not RAM. These need no `MEMW`: a commitment cell is written once and read by nobody, so there is no old value to produce and no timestamp to order. #render_constraint_table(chip, config, groups: "commit") -A committing row emits one interaction _per byte_, at index $#`dst` + i$, rather than one for the row. -The grouping is what forces that. -The verifier reconstructs this side of the bus from the committed output alone, and what it sees there is the concatenation of every commitment the program made --- not where one `write` ended and the next began. -It therefore cannot reproduce the prover's row schedule, which restarts at every system call: a guest committing four bytes and then four more sends eight one-byte rows where a verifier chunking the eight bytes it sees would expect a single wide row, and an honest proof would be rejected. -Addressing every byte by its own index leaves the two sides nothing to disagree about. -`commit_lane` is what keeps a one-byte row from committing the seven bytes it never read. +A committing row emits one interaction _per byte_, at index $#`dst` + i$, rather than one for the row, and the grouping is what forces that. +The verifier reconstructs this side of the bus from the committed output alone, where it sees the concatenation of every commitment the program made --- not where one `write` ended and the next began --- so it cannot reproduce the prover's row schedule, which restarts at every system call. +A guest committing four bytes and then four more sends eight one-byte rows where a verifier chunking the eight bytes it sees expects a single wide row, and an honest proof would be rejected. +Addressing every byte by its own index removes the grouping; `commit_lane` keeps a one-byte 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 that still have to be moved afterwards. @@ -186,7 +181,7 @@ We use the `end` bit to indicate these circumstances. #render_constraint_table(chip, config, groups: "end") *Note*: -+ As `COMMIT` used to (@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`. ++ 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, $ @@ -207,17 +202,14 @@ Both tuples carry the `timestamp`, and that is what separates one sequence from without it, rows belonging to two different sequences could be spliced into each other's while the bus still balances. Since the CPU's timestamps strictly increase per instruction, no two #memmove sequences share one. -Observe also that this chip has no constraint demanding that a sequence terminates. -It does not need one, but the reason is worth stating carefully, because the obvious counting argument is not sufficient on its own. - +This chip has no constraint demanding that a sequence terminates, and the reason it needs none is worth stating carefully, because the obvious counting argument is not sufficient on its own. Fix a timestamp. -Balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ caps the latter at one. +Balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ caps the number of rows claiming `first` at one. The `CPU` sends a single `ECALL` per timestamp, which is what caps @memmove:c:receive_ecall; and `COMMIT` puts at most one row on `COMMIT_DEFER` per timestamp, for the same reason, which is what caps @memmove:c:receive_commit_defer. The two are moreover exclusive, since that single `ECALL` cannot be both a copy and a `write`. 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 entry at all, and would still emit a read and a write per row. +That rules out an _open_ sequence and nothing more: a ring of rows carrying $#`μ` = 1$ with neither `first` nor `end` set sends and receives one tuple each, so it balances, consumes no entry, and would still emit a read and a write per row. What forbids the ring is @memmove:c:src_incr: `ADDNW` forces $#`src_incr` = #`src` + #`step`$ _over the integers_ with $#`step` >= 1$, so `src` strictly increases along the sequence and can never return to a value it already held. This is the second reason the positions use `ADDNW` rather than `ADD`, and the more important of the two. @@ -245,18 +237,32 @@ Because every row of the sequence writes at $#`timestamp` + 1$ and reads at $#`t The recursion bottoms out in the seed, which the sequence never wrote. None of this depends on how the prover schedules the widths. +The call carries one precondition beyond the gap itself: neither `src` nor `src` $+$ `count` may cross the $2^32$ limb boundary, for the reason given in the third bullet below. +This is a real restriction on the caller rather than a property the chip enforces --- the AIR simply has no satisfying assignment for such a call --- so the executor rejects it up front and the guest stub keeps its chunks clear of the boundary. + @memmove:c:set_gap_lo and @memmove:c:set_gap_hi pin the gap, and the pinning is load-bearing rather than a convention. The degenerate case is $#`dst` = #`src`$: the read and the write then address the same cell at two adjacent timestamps, the memory argument is satisfied by $#`value` = #`value`$, and all eight lanes become free field elements. Nothing else in this chip touches them --- they are typed as bytes but range-checked nowhere, because on a moving row @memmove:c:read_value pins them --- so a prover could put anything it liked into RAM, and hence into the committed output. Three details of the pinning are worth spelling out: -- The distance must be at least the width of the widest row, so $8$ is the smallest one that works. - At distance $1$ an eight-byte row's read range overlaps its own write range and the argument above returns. +- Only $#`dst` = #`src`$ frees the lanes; at a distance $d$ with $1 <= d <= 8$ a row still pins $#`value`_i = #`value`_(i-d)$ for $i >= d$, and pins the first $d$ lanes against memory it did not write. + The gap is $8$ because that is the width of the widest row, so a wide row's read range and its write range stay disjoint, and because it is the length of the seed the guest lays down. - The gate is `is_set` alone, and not `is_set` together with a multiplicity. - `step` advances `src` and `dst` together, so $#`dst` - #`src`$ is invariant along a sequence and the relation holds on the terminal row as well; a padding row leaves $#`is_set` = 0$. - Gating on a product would cost a degree, and this chip stays at degree 2. -- Taken together the two constraints force $#`dst` - #`src` = 8$ _in the field_, whichever way the prover splits the two addresses over their limbs, and that is already enough to rule out the aliasing. - Reading them as a gap of $8$ over the integers additionally needs @memmove:a:src and @memmove:a:dst, which the register file discharges on the first row and @memmove:c:range_src_incr and @memmove:c:range_dst_incr on every later one. + Gating on a product would cost a degree, and this chip stays at degree 2; a padding row leaves $#`is_set` = 0$, and the terminal row satisfies the relation for the same reason every other row does. +- The two constraints are _limb-wise_, and that is stronger than a gap of $8$ on the 64-bit value. + They admit no carry out of the low limb: $#`src` = (2^32 - 16, 0)$ with $#`dst` = (2^32 - 8, 0)$ satisfies them, but one eight-byte step sends `dst` to $(0, 1)$ while `src` stays in limb $0$, and the successor row satisfies neither. + An honest `memset` whose range crosses the $2^32$ limb boundary therefore has no satisfying assignment at all. + += The commitment index +On a commitment sequence `dst` is a byte index rather than an address, and `COMMIT` carries it as a `BaseField` (@commit), so @memmove:a:dst is not discharged there. +Two things in this chapter do lean on it, and both degrade rather than break. + +@memmove:c:dst_incr invokes `ADDNW`, whose @addnw:a:lhs _is_ that assumption: without it the template no longer forces $#`dst_incr` = #`dst` + #`step`$ over the integers, only the field statement, so a denormalized index admits a spurious carry into the high limb. +And the per-lane addresses of @memmove:c:commit_value_out are built as $#`dst`_0 + i$ without the carry normalisation `MEMW` applies to its own lanes (@memw), so a row with $#`dst`_0 > 2^32 - 8$ addresses its upper lanes outside the low limb. + +Neither is a gain for a prover, because a token of that shape has no receiver: the commitment domain is reached by no chip other than this one, and the verifier supplies exactly one $(2, a, 0, dot)$ token per index. +The argument that rules out a ring is unaffected, since it is a statement about `src`, which `COMMIT` does read from `x11`. +Both would be settled at the source by range-checking `index` where it enters `COMMIT`; note that with `count` unbounded on this path, @commit:c:read_index can also write a value past the `Word` range into `x254`. = The Accelerated Memory Operations standard The Ethereum Foundation's Accelerated Memory Operations standard fixes what an accelerated `memcpy`, `memmove` and `memset` must provide. @@ -267,6 +273,7 @@ The first is behavioural: the accelerated symbol must behave identically to the The second concerns linking: the symbol must be a strong definition in an unconditionally linked object, or be linked with `--whole-archive`, so that a weak definition elsewhere cannot silently displace it. What the standard asks of the chip itself is that it accept operands of arbitrary alignment, which it does: no constraint here refers to the alignment of `src`, `dst` or `count`, and a row's width is not tied to any of them. +The one operand restriction this chip does impose is not an alignment: a `memset` may not straddle the $2^32$ limb boundary, as described above. The standard's fourth operation, `memcmp`, is not covered: it does not copy, so it does not fit this chip, and accelerating it would need a table of its own. = Notes/optimizations @@ -279,12 +286,11 @@ The standard's fourth operation, `memcmp`, is not covered: it does not copy, so Only the seven lanes that a one-byte row leaves unused need @memmove:c:tail_lanes, since those never reach the read. On a row that moves nothing --- the terminal row, and padding rows --- there is no read, so $#`value`_0$ is an arbitrary field element there. That is harmless, because every write carries a multiplicity that vanishes with `end` and so does not fire either. -- @memmove:c:range_src_incr and @memmove: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. - It would not make the proof smaller, though: `IS_HALF` is answered by a preprocessed table whose height is fixed at compile time, so dropping lookups moves multiplicities and leaves the number of committed cells where it was. +- @memmove:c:range_src_incr and @memmove:c:range_dst_incr carry multiplicity $#`μ`$, but `src_incr` and `dst_incr` are _consumed_ only at $#`μ` - #`end`$ --- on a terminal row they are pinned by nothing beyond @addnw:c:carry, which holds unconditionally. + Lowering both to $#`μ` - #`end`$ would drop eight `IS_HALF` lookups on every terminal row at no cost, though not a smaller proof: that table is preprocessed at a fixed height, so the committed cell count is unchanged. @memmove:c:range_count_decr genuinely needs $#`μ`$, since @memmove:c:end consumes `count_decr` at that multiplicity. - A row could move sixteen or thirty-two bytes rather than eight, at the cost of a wider `MEMW` signature. - It would also narrow the aligned fast path: `MEMW_A` admits an access only when it is aligned to its own width, so sixteen-byte rows would need sixteen-byte-aligned ends to stay on the cheap chip, and the widths `MEMW`'s signature can express today are one, two, four and eight. + It would also narrow the fast path: `MEMW_A` needs every byte of an access to share one old timestamp, which a sixteen-byte row can only manage where the buffer was last written in groups at least that wide, and the widths `MEMW`'s signature can express today are one, two, four and eight. Rows saved and cells saved therefore move in opposite directions here, and only the second is what the proof pays for. -- The `memmove` property belongs to one `ECALL`, not to an arbitrarily large guest-level copy: a copy larger than 256 bytes is split by the guest stub into several `ECALL`s at distinct timestamps, and chunk $k+1$ reads what chunk $k$ has already written. - That is in-contract for `memcpy`, whose buffers may not overlap; a guest-side `memmove` has to keep each copy within a single `ECALL`, or chunk in the direction that preserves the semantics. +- The `memmove` property belongs to one `ECALL`, not to an arbitrarily large guest-level copy: past 256 bytes the stub splits into several `ECALL`s at distinct timestamps, and chunk $k+1$ reads what chunk $k$ wrote. + That is in-contract for `memcpy`, whose buffers may not overlap; a guest-side `memmove` must keep each copy within one `ECALL` or chunk in the direction that preserves the semantics. diff --git a/spec/meta.typ b/spec/meta.typ index dada8202d..ee862f8ee 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -49,9 +49,9 @@ ("commit", [`COMMIT` chip], ), ("sha256", [`SHA256` accelerator], ), ("keccak", [`KECCAK` accelerator], ), - ("memmove", [`MEMMOVE` accelerator], ), ("ecsm", [`ECSM` accelerator], ), ("fext", [Extension field accelerator], ), + ("memmove", [`MEMMOVE` accelerator], ), )), ("MATHEMATICS", ( ("limbs_and_carries", [On limb decomposition and carries], ), diff --git a/spec/src/memmove.toml b/spec/src/memmove.toml index e759fc4d1..eeafb4b4b 100644 --- a/spec/src/memmove.toml +++ b/spec/src/memmove.toml @@ -1,4 +1,5 @@ name = "MEMMOVE" +code = "MMV" # Input @@ -67,7 +68,7 @@ pad = 1 [[variables.auxiliary]] name = "short" type = "Bit" -desc = "Whether $#`count` < 8$, i.e. whether eight bytes are still available to move." +desc = "Whether $#`count` < 8$, i.e. whether this row may not move eight bytes." pad = 1 [[variables.auxiliary]] @@ -111,7 +112,7 @@ pad = 0 [[variables.virtual]] name = "step" type = "Byte" -desc = "The stride this row advances by: eight, or one when `tail` is set. No bytes are moved on the terminal row." +desc = "The stride this row advances by: eight, or one when `tail` is set." def = ["-", 8, ["*", 7, "tail"]] [[variables.virtual]] From 538a5d7f22cc8170034c7bbf6f8429a89c83bcc2 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 11 Sep 2026 10:33:04 -0300 Subject: [PATCH 3/4] tighten the chapter --- spec/chapters/memmove.typ | 258 ++++++++++---------------------------- 1 file changed, 66 insertions(+), 192 deletions(-) diff --git a/spec/chapters/memmove.typ b/spec/chapters/memmove.typ index e5aa62844..d3142a589 100644 --- a/spec/chapters/memmove.typ +++ b/spec/chapters/memmove.typ @@ -1,4 +1,3 @@ -#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -15,10 +14,8 @@ #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 single copying primitive of this VM: one chip serves `memcpy`, `memmove`, `memset` and the byte loop of a commitment. +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-pages on `memmove`, `memcpy` and `memset`; man7.org. #link("https://man7.org/linux/man-pages/man3/memmove.3.html")[[src]]]) -Without it the guest would run these loops in RISC-V --- per doubleword a load, a store, two pointer increments and a branch, five instructions the proof pays for. - The three functionalities differ only in where the bytes go and in which of the two accesses happens first: #figure( @@ -33,8 +30,7 @@ The three functionalities differ only in where the bytes go and in which of the caption: [The three functionalities of #memmove.], ) -Neither the destination domain nor the order of the two accesses is chosen by the caller. -Both are derived from `is_set` and `is_commit`, and those two bits are in turn decoded from the way the sequence was entered. +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) @@ -47,37 +43,24 @@ The #memmove chip is comprised of #nr_variables variables that are expressed usi = Assumptions #render_chip_assumptions(chip, config) -These assumptions concern the _first_ row of a sequence. -There, `src`, `dst` and `count` come either from the register file or from `COMMIT`, and `timestamp` from the `CPU`. -Every later row receives all four over the `MEMMOVE_NEXT` bus, where @memmove:c:range_src_incr, @memmove:c:range_dst_incr and @memmove:c:range_count_decr range-check three of them on the sending side. -The fourth, `timestamp`, is range-checked by neither side; it holds because the value travels unchanged from the `ECALL` at the root of the sequence, which is where @memmove:a:timestamp is discharged. - -@memmove:a:dst is not discharged on a commitment sequence; that case is taken up at the end of this chapter. +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, where `dst` is an index that `COMMIT` carries as a `BaseField`; see the notes below. = Constraints -This VM assigns system call number $-30$ to the copy functionality 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. -A sequence is therefore entered exactly once, and only that first row accepts an entry. -There are two ways in: from the `CPU`, by accepting an `ECALL`, or from `COMMIT`, which keeps the `write` system call for itself and defers only the byte loop. +In this VM, we assign system call number $-30$ to the copy functionality 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_defer` 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`$, a linear function of the selector, so `is_set` is decoded from the `ECALL` the guest actually executed rather than chosen by the prover. -`is_commit` is decoded from _which_ bus the first row accepted from: `COMMIT_DEFER` has exactly one sender, and that is `COMMIT`. - -#aside("The syscall number alone does not pin the selector")[ - The low limb of @memmove:c:receive_ecall is a line in `is_set` and so runs over the whole field, while the high limb is the constant $2^32 - 1$. - Every system call number in the negative range is therefore reproduced by some field element, and @memmove:c:range_is_set is what rules those out --- it carries the whole decoding argument. - This matters when `ECALL` numbers are allocated (@ecall): a negative number is safe from this chip because `is_set` is a bit, never because it is far away from $-30$ and $-32$. -] - -@memmove:c:one_hot makes the two selectors mutually exclusive and @memmove:c:functionality_implies_mu keeps both clear on a padding row. -Both selectors also ride _inside_ the `MEMMOVE_NEXT` tuple in either direction (@memmove:c:send_next_chunk, @memmove:c:receive_next_chunk), so a sequence cannot change functionality half way through it. +@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 of these define nothing new; they combine a selector with `first`, with $#`μ` - #`end`$, and with `tail` respectively. -They exist as columns because a multiplicity has to be linear in the columns of the chip (@logup), and a product of two of them is not. -The remaining combinations, `first_defer` and `ram_write`, are differences of columns and so need no column of their own. +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: @@ -86,211 +69,102 @@ The guest-side `memcpy` this chip accelerates has the following signature: 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` contains the address of the first byte to read, and -- `A2` contains `count`; the number of bytes to move. - -`memset` uses the same three registers for the same three roles --- `A1` is a source address there too, not a fill byte --- and what the guest puts in them is discussed at the bottom of this chapter. -@memmove:c:read_dst, @memmove:c:read_src and @memmove:c:read_count read the three registers. -Each of them writes back the value that was read, so the operation leaves the registers untouched; -the guest is responsible for producing the return value. -These reads are conditioned on `first_ecall`: a deferred commitment sequence takes its operands from `COMMIT` instead, which has already read the registers of the `write` system call. +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 $#`short` = (#`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 left free: the prover may cut any row down to a single byte. -That freedom is what lets a schedule choose where its wide rows fall, which is what decides whether they are admitted by `MEMW_A` rather than by the wider `MEMW` (@memw). -Which schedule is used is a prover-side choice; the AIR grants the freedom and charges for the rows. - -Because a row is the unit in which this chip charges, an unbounded `count` would let a single guest instruction append an unbounded number of rows to the trace. -@memmove:c:bound therefore proves $#`count` < 257$ on the first row of every `ECALL`-entered sequence, which caps it at $257$ rows --- the bound is the one-byte-per-row schedule, not the honest one. -The guest-side stubs chunk larger operations into multiple `ECALL`s; the executor rejects any chunk exceeding 256 bytes. +@memmove:c:short pins $#`short` = (#`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 at all --- and `COMMIT` range-checks no `count` either. -No prover gain follows: the commitment bus still has to balance against the committed output, which the verifier knows in full, so a sequence can only be as long as the output it produces. -What it does cost is work, and not only the prover's --- the verifier contributes a token pair per committed byte --- so a `write` with an absurd `count` is unprovable and unverifiable rather than merely expensive. - -#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 eight 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. -] +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 absurd `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`$: the two accesses are one timestamp apart, and `is_set` decides which of them comes first. -The `CPU`'s preprocessed timestamp column holds $4 dot (i + 1)$ at row $i$ (@vars), so neither expression can leave the `Word` range --- `IS_WORD` on `timestamp` alone would not rule that out. -Both interactions are expressed over the _same_ `value` variable, which is what makes the moved 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`. +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. -With the normal order that makes every read observe memory as it was before the sequence started, which is precisely `memmove`'s guarantee for an overlapping range. -With the order inverted every read instead observes memory after all of the sequence's writes, and the sequence propagates rather than copies; that is `memset`, and @memmove:c:set_gap_lo and @memmove:c:set_gap_hi are what make it well-defined. -Both orders keep the read and the write at distinct timestamps and both strictly after `timestamp`, so the memory argument is undisturbed either way. +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:tail_lanes canonicalises a one-byte row, which addresses `MEMW` with $#`write2` = #`write4` = #`write8` = 0$. -`MEMW` gates lane $i >= 1$ on those same flags (@memw), so the seven unused lanes never reach the memory argument --- but they do reach the `MEMW` tuple, and pinning them to zero is what keeps it the canonical encoding of a single-byte access rather than one carrying seven free field elements. - -Which memory chip the two accesses reach is decided by their addresses, and this chip constrains neither. -`MEMW_A` is the fast path (@memw): it stores a single old timestamp, so it needs one `LT` row (@lt) to order the access, where the general `MEMW` stores one per byte and needs eight, on a row that is the wider of the two to begin with. -Two conditions admit an access there, and neither is the eight-byte alignment of its address: the access must not cross a $2^16$ limb boundary, and all the bytes it touches must carry the same old timestamp. -Alignment matters only through the second: a buffer last written in eight-byte aligned groups has one timestamp per group, so an eight-byte access that sits on a group reads one timestamp and an access that straddles two reads two. -That is what a schedule is buying when it spends one-byte rows to move a wide row onto a group boundary, and it is a property of how the buffer was written rather than of this chip. -The read and the write are routed independently, so a sequence can take the fast path at one end and not at the other, and the row counts this chapter reasons about are therefore not on their own the cost of an operation. +@memmove:c:set_gap_lo and @memmove:c:set_gap_hi pin that gap, and they are load-bearing: 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 the destination is not RAM. -`dst` is then the index of the byte in the committed output rather than an address#footnote[ - For very large commitments (with index $>= 2^32$), the commitment-domain address can become denormalized, but since no other chip interacts with this memory domain, there is no issue. - The usual consistency guarantee from the LogUp argument and correct initialization as for general addresses applies. -], and the write goes to a domain-separated part of memory with domain 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. +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 therefore gated on `ram_write` and does not fire, and @memmove:c:commit_value_out and @memmove:c:commit_value_in take its place. -These need no `MEMW`: a commitment cell is written once and read by nobody, so there is no old value to produce and no timestamp to order. +@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") -A committing row emits one interaction _per byte_, at index $#`dst` + i$, rather than one for the row, and the grouping is what forces that. -The verifier reconstructs this side of the bus from the committed output alone, where it sees the concatenation of every commitment the program made --- not where one `write` ended and the next began --- so it cannot reproduce the prover's row schedule, which restarts at every system call. -A guest committing four bytes and then four more sends eight one-byte rows where a verifier chunking the eight bytes it sees expects a single wide row, and an honest proof would be rejected. -Addressing every byte by its own index removes the grouping; `commit_lane` keeps a one-byte row from committing the seven bytes it never read. +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 that still have to be moved afterwards. +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") -Note the asymmetry between the two position updates and the count update: - -+ 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 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 moving 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 @memmove:c:send_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 because $#`step` <= #`count`$ on every row with $#`count` >= 1$: a wide row needs $#`short` = 0$ by @memmove:c:wide_needs_eight and hence $#`count` >= 8 = #`step`$, and a narrow row has $#`step` = 1$. - The subtraction can therefore only wrap on the terminal row. +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 $#`short` = 0$ and hence $#`count` >= 8 = #`step`$, and a narrow row has $#`step` = 1$. == Terminating the sequence -When `count` hits $0$, we should stop performing further recursive calls. -We use the `end` bit to indicate these circumstances. +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 in [0, 3]: #`count_decr`_i = 65535 - $ - 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 the read and both writes carry a multiplicity that vanishes with `end`, a row that wrongly claims `end` emits no memory operations at all, which is a silently truncated operation with every bus balanced. -+ $#`end` = 1$ still forces $#`count` = 0$ even though the prover picks the width. - The other candidate is $#`count` = 7$ with a wide row, which wraps `count_decr` to $2^64 - 1$; but $#`count` = 7$ gives $#`short` = 1$, and @memmove:c:wide_needs_eight then rejects the wide row. -+ An operation on zero bytes is a single row with $#`first` = #`end` = 1$: it accepts the entry and reads the three registers, but emits no memory operations and starts no recursion. ++ $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 $#`short` = 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 of this sequence, we recursively move the next chunk over the `MEMMOVE_NEXT` bus, specifying the timestamp, the positions to continue reading and writing at, the number of bytes that still have to be moved, and the functionality (@memmove:c:send_next_chunk). -Since that certainly won't be the `first` row of the sequence, we read `src_incr`, `dst_incr` and `count_decr` from the previous recursion level into `src`, `dst` and `count`, and continue. +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. #render_constraint_table(chip, config, groups: "lookups") -Both tuples carry the `timestamp`, and that is what separates one sequence from another: -without it, rows belonging to two different sequences could be spliced into each other's while the bus still balances. -Since the CPU's timestamps strictly increase per instruction, no two #memmove sequences share one. - -This chip has no constraint demanding that a sequence terminates, and the reason it needs none is worth stating carefully, because the obvious counting argument is not sufficient on its own. -Fix a timestamp. -Balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ caps the number of rows claiming `first` at one. -The `CPU` sends a single `ECALL` per timestamp, which is what caps @memmove:c:receive_ecall; and `COMMIT` puts at most one row on `COMMIT_DEFER` per timestamp, for the same reason, which is what caps @memmove:c:receive_commit_defer. -The two are moreover exclusive, since that single `ECALL` cannot be both a copy and a `write`. -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 rules out an _open_ sequence and nothing more: a ring of rows carrying $#`μ` = 1$ with neither `first` nor `end` set sends and receives one tuple each, so it balances, consumes no entry, and would still emit a read and a write per row. -What forbids the ring is @memmove:c:src_incr: `ADDNW` forces $#`src_incr` = #`src` + #`step`$ _over the integers_ with $#`step` >= 1$, so `src` strictly increases along the sequence and can never return to a value it already held. -This is the second reason the positions use `ADDNW` rather than `ADD`, and the more important of the two. +This chip has no constraint demanding that a sequence terminates, and the reason it needs none is worth stating, because the counting argument alone is not sufficient. +Fix a timestamp: balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ 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, we must make sure the seven independent bits are bits, and that either $#`first` = 1$ or $#`end` = 1$ implies $#`μ` = 1$ (@memmove:c:first_or_end_implies_mu). -The latter is required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary. -`first_ecall`, `commit_write` and `commit_write_wide` need no range check of their own: the constraints of @memmove:c:first_ecall, @memmove:c:commit_write and @memmove:c:commit_write_wide already equate each of them to a product of 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) -Note that this padding row is not all-zero. -@memmove: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. -$#`tail` = 1$ in turn satisfies @memmove:c:wide_needs_eight for either value of `short`. -The two position 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. - -= `memset` as a propagating `memmove` -`memset` needs no machinery of its own beyond the inverted order, but it does need the guest to hand it the right operands. - -The stub seeds the first eight bytes of the range with ordinary stores and then calls the accelerator with `src` the start of that seed, `dst` its end and `count` the remaining length; fills shorter than sixteen bytes take a plain store loop instead, since they cannot amortise the seed. -The row at offset $k$ then reads at $#`src` + k$ and writes at $#`src` + k + 8$. -Because every row of the sequence writes at $#`timestamp` + 1$ and reads at $#`timestamp` + 2$, each read observes the whole sequence's writes, so the row forces $"mem"[#`src` + k + 8] = "mem"[#`src` + k]$ for every $k$, and the eight seeded bytes are replicated across the range. -The recursion bottoms out in the seed, which the sequence never wrote. -None of this depends on how the prover schedules the widths. - -The call carries one precondition beyond the gap itself: neither `src` nor `src` $+$ `count` may cross the $2^32$ limb boundary, for the reason given in the third bullet below. -This is a real restriction on the caller rather than a property the chip enforces --- the AIR simply has no satisfying assignment for such a call --- so the executor rejects it up front and the guest stub keeps its chunks clear of the boundary. +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. -@memmove:c:set_gap_lo and @memmove:c:set_gap_hi pin the gap, and the pinning is load-bearing rather than a convention. -The degenerate case is $#`dst` = #`src`$: the read and the write then address the same cell at two adjacent timestamps, the memory argument is satisfied by $#`value` = #`value`$, and all eight lanes become free field elements. -Nothing else in this chip touches them --- they are typed as bytes but range-checked nowhere, because on a moving row @memmove:c:read_value pins them --- so a prover could put anything it liked into RAM, and hence into the committed output. - -Three details of the pinning are worth spelling out: -- Only $#`dst` = #`src`$ frees the lanes; at a distance $d$ with $1 <= d <= 8$ a row still pins $#`value`_i = #`value`_(i-d)$ for $i >= d$, and pins the first $d$ lanes against memory it did not write. - The gap is $8$ because that is the width of the widest row, so a wide row's read range and its write range stay disjoint, and because it is the length of the seed the guest lays down. -- The gate is `is_set` alone, and not `is_set` together with a multiplicity. - Gating on a product would cost a degree, and this chip stays at degree 2; a padding row leaves $#`is_set` = 0$, and the terminal row satisfies the relation for the same reason every other row does. -- The two constraints are _limb-wise_, and that is stronger than a gap of $8$ on the 64-bit value. - They admit no carry out of the low limb: $#`src` = (2^32 - 16, 0)$ with $#`dst` = (2^32 - 8, 0)$ satisfies them, but one eight-byte step sends `dst` to $(0, 1)$ while `src` stays in limb $0$, and the successor row satisfies neither. - An honest `memset` whose range crosses the $2^32$ limb boundary therefore has no satisfying assignment at all. - -= The commitment index -On a commitment sequence `dst` is a byte index rather than an address, and `COMMIT` carries it as a `BaseField` (@commit), so @memmove:a:dst is not discharged there. -Two things in this chapter do lean on it, and both degrade rather than break. - -@memmove:c:dst_incr invokes `ADDNW`, whose @addnw:a:lhs _is_ that assumption: without it the template no longer forces $#`dst_incr` = #`dst` + #`step`$ over the integers, only the field statement, so a denormalized index admits a spurious carry into the high limb. -And the per-lane addresses of @memmove:c:commit_value_out are built as $#`dst`_0 + i$ without the carry normalisation `MEMW` applies to its own lanes (@memw), so a row with $#`dst`_0 > 2^32 - 8$ addresses its upper lanes outside the low limb. - -Neither is a gain for a prover, because a token of that shape has no receiver: the commitment domain is reached by no chip other than this one, and the verifier supplies exactly one $(2, a, 0, dot)$ token per index. -The argument that rules out a ring is unaffected, since it is a statement about `src`, which `COMMIT` does read from `x11`. -Both would be settled at the source by range-checking `index` where it enters `COMMIT`; note that with `count` unbounded on this path, @commit:c:read_index can also write a value past the `Word` range into `x254`. += Notes/potential optimizations +- On a commitment sequence @memmove:a:dst is undischarged, 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 commitment addresses 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`. +- `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. @memmove:c:range_count_decr genuinely needs $#`μ`$. +- 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 decoded into `MEMW`'s width flags. +- 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. = 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. #link("https://github.com/eth-act/zkevm-standards/tree/main/standards/accelerated-memory-operations")[[src]]]) - -Two of its requirements fall outside this chapter. -The first is behavioural: the accelerated symbol must behave identically to the C library function, which the guest-side stub is responsible for. -The second concerns linking: the symbol must be a strong definition in an unconditionally linked object, or be linked with `--whole-archive`, so that a weak definition elsewhere cannot silently displace it. - -What the standard asks of the chip itself is that it accept operands of arbitrary alignment, which it does: no constraint here refers to the alignment of `src`, `dst` or `count`, and a row's width is not tied to any of them. -The one operand restriction this chip does impose is not an alignment: a `memset` may not straddle the $2^32$ limb boundary, as described above. -The standard's fourth operation, `memcmp`, is not covered: it does not copy, so it does not fit this chip, and accelerating it would need a table of its own. - -= Notes/optimizations -- `COMMIT` could send its deferral on `MEMMOVE_NEXT` directly, with $#`is_commit` = 1$ in the tuple, which would retire the `COMMIT_DEFER` bus and the `first_ecall` column. - A commitment sequence would then have no `first` row at all, so `first` would come to mean "entered by `ECALL`" rather than "head of the sequence", and $#`first` dot #`is_commit` = 0$ would have to be added to stop an `ECALL`-entered sequence from writing to the commitment domain. -- `count` need not be a full `DWordWL` on the `ECALL` path: @memmove:c:bound already proves $#`count` < 257$ there, and every later `count` is smaller still. - The commitment path has no such bound, so this would have to be paid for with a range check where the value enters from `COMMIT`. -- The `value` variable is typed as bytes, but this chip range-checks none of its lanes. - On a row that moves, they are pinned by @memmove: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 @memmove:c:tail_lanes, since those never reach the read. - On a row that moves nothing --- the terminal row, and padding rows --- there is no read, so $#`value`_0$ is an arbitrary field element there. - That is harmless, because every write carries a multiplicity that vanishes with `end` and so does not fire either. -- @memmove:c:range_src_incr and @memmove:c:range_dst_incr carry multiplicity $#`μ`$, but `src_incr` and `dst_incr` are _consumed_ only at $#`μ` - #`end`$ --- on a terminal row they are pinned by nothing beyond @addnw:c:carry, which holds unconditionally. - Lowering both to $#`μ` - #`end`$ would drop eight `IS_HALF` lookups on every terminal row at no cost, though not a smaller proof: that table is preprocessed at a fixed height, so the committed cell count is unchanged. - @memmove:c:range_count_decr genuinely needs $#`μ`$, since @memmove:c:end consumes `count_decr` at that multiplicity. -- A row could move sixteen or thirty-two bytes rather than eight, at the cost of a wider `MEMW` signature. - It would also narrow the fast path: `MEMW_A` needs every byte of an access to share one old timestamp, which a sixteen-byte row can only manage where the buffer was last written in groups at least that wide, and the widths `MEMW`'s signature can express today are one, two, four and eight. - Rows saved and cells saved therefore move in opposite directions here, and only the second is what the proof pays for. -- The `memmove` property belongs to one `ECALL`, not to an arbitrarily large guest-level copy: past 256 bytes the stub splits into several `ECALL`s at distinct timestamps, and chunk $k+1$ reads what chunk $k$ wrote. - That is in-contract for `memcpy`, whose buffers may not overlap; a guest-side `memmove` must keep each copy within one `ECALL` or chunk in the direction that preserves the semantics. +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. From 35ce3efa61f81d519e6463462399c61804bd3781 Mon Sep 17 00:00:00 2001 From: Nicole Date: Fri, 11 Sep 2026 11:42:54 -0300 Subject: [PATCH 4/4] Align the chapter with conventions --- spec/chapters/memmove.typ | 71 ++++++++++++++++++++------------------- spec/src/commit.toml | 4 +-- spec/src/memmove.toml | 50 +++++++++++++-------------- 3 files changed, 64 insertions(+), 61 deletions(-) diff --git a/spec/chapters/memmove.typ b/spec/chapters/memmove.typ index d3142a589..60037f202 100644 --- a/spec/chapters/memmove.typ +++ b/spec/chapters/memmove.typ @@ -1,3 +1,4 @@ +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -15,20 +16,16 @@ 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-pages on `memmove`, `memcpy` and `memset`; man7.org. #link("https://man7.org/linux/man-pages/man3/memmove.3.html")[[src]]]) +#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: -#figure( - table( - columns: 5, - align: left, - table.header[*functionality*][*entered by*][*destination*][*read at*][*write at*], - [`memcpy`/`memmove`], [`ECALL` $-30$], [RAM], [$#`timestamp` + 1$], [$#`timestamp` + 2$], - [`memset`], [`ECALL` $-32$], [RAM], [$#`timestamp` + 2$], [$#`timestamp` + 1$], - [`commit`], [`COMMIT` (@commit)], [commitment domain], [$#`timestamp` + 1$], [---], - ), - caption: [The three functionalities of #memmove.], -) +#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. @@ -45,12 +42,12 @@ The #memmove chip is comprised of #nr_variables variables that are expressed usi 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, where `dst` is an index that `COMMIT` carries as a `BaseField`; see the notes below. +@memmove:a:dst is not discharged at all on a commitment sequence (@memmove:aside:index). = Constraints -In this VM, we assign system call number $-30$ to the copy functionality and $-32$ to `memset`. +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_defer` split `first` between them. +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 @@ -76,13 +73,13 @@ These are conditioned on `first_ecall`, since a deferred commitment sequence tak == Chunk width A row moves eight bytes, or a single byte when `tail` is set. -@memmove:c:short pins $#`short` = (#`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. +@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 absurd `count` is unverifiable as well as unprovable. +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. @@ -95,7 +92,7 @@ Every row of a sequence carries the same `timestamp`, so an entire sequence read 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, and they are load-bearing: 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. +@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. @@ -108,6 +105,11 @@ When `is_commit` is set, `dst` is the index of the byte in the committed output @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: )[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. @@ -118,7 +120,7 @@ The first two of @memmove:c:range_src_incr, @memmove:c:range_dst_incr and @memmo 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 $#`short` = 0$ and hence $#`count` >= 8 = #`step`$, and a narrow row has $#`step` = 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. @@ -128,18 +130,20 @@ When `count` hits $0$ we stop recursing, which the `end` bit indicates. + 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 $#`short` = 1$ and is rejected by @memmove:c:wide_needs_eight. ++ $#`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") -This chip has no constraint demanding that a sequence terminates, and the reason it needs none is worth stating, because the counting argument alone is not sufficient. -Fix a timestamp: balancing `MEMMOVE_NEXT` forces the number of rows claiming `end` to equal the number claiming `first`, and $#`first` = #`first_ecall` + #`first_defer`$ 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. +#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. @@ -153,18 +157,17 @@ To pad this chip, use the below data. 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. -= Notes/potential optimizations -- On a commitment sequence @memmove:a:dst is undischarged, 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 commitment addresses 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`. -- `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. @memmove:c:range_count_decr genuinely needs $#`μ`$. -- 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 decoded into `MEMW`'s width flags. -- 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. - = 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. #link("https://github.com/eth-act/zkevm-standards/tree/main/standards/accelerated-memory-operations")[[src]]]) +#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/src/commit.toml b/spec/src/commit.toml index d9caa9d21..73d3d347e 100644 --- a/spec/src/commit.toml +++ b/spec/src/commit.toml @@ -12,13 +12,13 @@ pad = 0 [[variables.auxiliary]] name = "index" type = "BaseField" -desc = "Index of the first value being committed by this sequence." +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]] diff --git a/spec/src/memmove.toml b/spec/src/memmove.toml index eeafb4b4b..bf25e244d 100644 --- a/spec/src/memmove.toml +++ b/spec/src/memmove.toml @@ -14,7 +14,7 @@ pad = 0 [[variables.auxiliary]] name = "src" type = "DWordWL" -desc = "Address of the first byte read by this row." +desc = "Address of the first byte read by this row" pad = 0 [[variables.auxiliary]] @@ -26,7 +26,7 @@ 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." +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]] @@ -38,7 +38,7 @@ pad = 1 [[variables.auxiliary]] name = "count" type = "DWordWL" -desc = "Number of bytes that still have to be moved, including those moved by this row." +desc = "Number of bytes that still have to be moved, including those moved by this row" pad = 1 [[variables.auxiliary]] @@ -50,61 +50,61 @@ pad = ["arr", 0, 0, 0, 0] [[variables.auxiliary]] name = "first" type = "Bit" -desc = "Whether this is the first row of this sequence." +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." +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." +desc = "Whether this row moves a single byte rather than eight" pad = 1 [[variables.auxiliary]] -name = "short" +name = "count_lt8" type = "Bit" -desc = "Whether $#`count` < 8$, i.e. whether this row may not move eight bytes." +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." +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." +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`." +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." +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." +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." +desc = "The bytes moved by this row; only $#`value`_0$ is moved when $#`tail` = 1$. Unconstrained on rows that move nothing" pad = 0 # Virtual @@ -112,25 +112,25 @@ pad = 0 [[variables.virtual]] name = "step" type = "Byte" -desc = "The stride this row advances by: eight, or one when `tail` is set." +desc = "The stride this row advances by: eight, or one when `tail` is set" def = ["-", 8, ["*", 7, "tail"]] [[variables.virtual]] -name = "first_defer" +name = "first_commit" type = "Bit" -desc = "$#`first` dot #`is_commit`$; whether this row is the first of a sequence deferred by `COMMIT`." +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." +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." +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"}, @@ -181,7 +181,7 @@ ref = "memmove:c:receive_ecall" kind = "interaction" tag = "COMMIT_DEFER" input = ["timestamp", "src", "dst", "count"] -multiplicity = ["-", "first_defer"] +multiplicity = ["-", "first_commit"] ref = "memmove:c:receive_commit_defer" [[constraint_groups]] @@ -251,14 +251,14 @@ name = "width" kind = "interaction" tag = "ALU" input = ["count", ["cast", 8, "DWordWL"], ["opsel", "LT"]] -output = ["arr", "short", 0] +output = ["arr", "count_lt8", 0] multiplicity = "μ" ref = "memmove:c:short" [[constraints.width]] kind = "arith" -constraint = "$#`short` => #`tail` = 1$" -poly = ["*", ["not", "tail"], "short"] +constraint = "$#`count_lt8` => #`tail` = 1$" +poly = ["*", ["not", "tail"], "count_lt8"] ref = "memmove:c:wide_needs_eight" [[constraints.width]] @@ -410,8 +410,8 @@ ref = "memmove:c:range_tail" [[constraints.bits]] kind = "template" tag = "IS_BIT" -input = ["short"] -ref = "memmove:c:range_short" +input = ["count_lt8"] +ref = "memmove:c:range_count_lt8" [[constraints.bits]] kind = "template"