diff --git a/spec/chapters/about_ecalls.typ b/spec/chapters/about_ecalls.typ index 102d7a504..4c2e82738 100644 --- a/spec/chapters/about_ecalls.typ +++ b/spec/chapters/about_ecalls.typ @@ -26,7 +26,7 @@ where `A0`-`A7` are symbolic names for the registers `x10`-`x17` We provide a list of supported ECALL numbers. Negative numbers (represented as 2s complement 64-bit numbers), are used for our own custom accelerators/extensions. -/ 64: `write` (@commit) +/ 64: `write` (@copy) / 93: `exit` (@halt) / -1: `SHA256` (@sha256) / -2: `KECCAK` (@keccak) @@ -35,3 +35,20 @@ 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: `memcpy`/`memmove` (@copy) +/ -31: `memset` (@copy) + +== Committing to values + +To make a claim about a public value to the verifier, a guest program can _commit_ to it. +In this VM, this is achieved by writing to `stdout`, with a write syscall to file descriptor 1. +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[ + 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. +] +In doing this, we enforce that all values being committed match the claimed commitment. +The verifier should additionally check that register 254 contains the total number of bytes committed. +The technical details on how the copy to memory domain 2 is achieved can be found in @copy, where `write` is implemented. diff --git a/spec/chapters/commit.typ b/spec/chapters/commit.typ deleted file mode 100644 index 14aa1dedc..000000000 --- a/spec/chapters/commit.typ +++ /dev/null @@ -1,124 +0,0 @@ -#import "/meta.typ": aside -#import "/src.typ": load_config, load_chip -#import "/chip.typ": ( - render_chip_variable_table, - total_nr_variables, - total_nr_instantiated_columns, - compute_nr_interactions, - render_constraint_table, - render_chip_assumptions, - render_chip_padding_table, -) - -#let config = load_config() -#let chip = load_chip("src/commit.toml", config) -#let commit = raw(chip.name) - -= Variables -#let nr_variables = total_nr_variables(chip) -#let nr_columns = total_nr_instantiated_columns(chip, config) -#let nr_interactions = compute_nr_interactions(chip) - -The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: -#render_chip_variable_table(chip, config) - -= Constraints -In this VM, committing is considered equivalent to writing a value to `stdout`. -Hence, this chip responds to `ECALL`s with system call number 64. -#footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L174")[[src]]]) -Since we do not know how many bytes are to be committed, this chip employs a recursive design: -each iteration commits one byte, and recursively "calls" itself to commit the remaining bytes. -As such, only the call from the CPU to this chip (i.e., the `first` in the recursion tree) should accept the `ECALL`; later recursive calls should not. -This is why @commit:c:receive_ecall has multiplicity $-#`first`$. -#render_constraint_table(chip, config, groups: "incoming") - -The `write` operation --- writing to a file descriptor --- has the following signature: -#footnote([Linux man-page on `write`; man7.org, version 6.16, 2025-10-29. #link("https://man7.org/linux/man-pages/man2/write.2.html")[[src]]]) - -```c -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, -- `A2` contains `count`, and -- the written count should be written to `A0`. - -@commit:c:read_address reads `address` from `x11` (=`A1`) and @commit:c:read_count reads `count` from `x12` (=`A2`). -Since we only support writing to `stdout` (which corresponds to $#`fd` = 1$ -#footnote([The Open Group Standard for Information Technology --- Portable Operating System Interface (POSIX) Base Specifications, `unistd.h`; The Open Group, issue 8, #link("https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/unistd.h.html")[[src]]])) -we assert that `x10` contains $1$ in @commit:c:read_fd_write_count. -Note that this constraint _also_ writes `count` to `A0`; -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. - -#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. -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. -#render_constraint_table(chip, config, groups: "bits") - -= Padding -To pad this chip, use the below data. -#render_chip_padding_table(chip, config) - -= 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. diff --git a/spec/chapters/copy.typ b/spec/chapters/copy.typ new file mode 100644 index 000000000..329026d32 --- /dev/null +++ b/spec/chapters/copy.typ @@ -0,0 +1,215 @@ +#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/copy.toml", config) +#let copy = raw(chip.name) + +The #copy chip copies a range of bytes from one location to another. +This single chip serves the standard `C` memory functions `memcpy`, `memmove` and +(a variation to#footnote[See @reading-parameters]) `memset`, as well as the `write` syscall. + += 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 #copy 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 +#render_chip_assumptions(chip, config) + += Constraints +The behaviour of this chip is slightly different, depending on the exact +function it is expected to perform. +The only exception here are `memcpy` and `memmove`: the definition of `memmove` +subsumes that of `memcpy`, meaning that we can perform both operation in the same way. +As such, this chip need only distinguish three states. +This is achieved by means of the `is_write` and `is_set` flags, +which are to be set according to the below table. +Importantly, the `is_write` and `is_set` flags are not to be set simultaneously, +as enforced by @copy:c:one_hot. + +#figure( + table( + stroke: none, + columns: (auto, auto, auto), + align: (right, center, center), + table.header( + [], [`is_write`], [`is_set`], + ), + table.hline(), + table.vline(x: 1), + [`memmove`/`memcpy`], [0], [0], + [`memset`], [0], [1], + [`write`], [1], [0], + [-], [1], [1], + ) +) + +#render_constraint_table(chip, config, groups: "flags") + +== Receiving `ECALL` + +Each of the three chip states corresponds to a syscall number: $-30$ for `memmove`/`memcpy`, $-31$ for `memset`, and $64$ to `write`.#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]]]) +The chip is to accept `ECALL`s with all three of these numbers. +Rather than having a separate interactions for each, this chip leverages the +prover-hinted `is_write` and `is_set` flags to extract the correct syscall number from the bus: + +#render_constraint_table(chip, config, groups: "ecall") + +Note that this step is performed exactly when the prover-hinted `first` flag is set, +ensuring this flag is only set on the first row of a copy sequence. + +== Reading parameters + +Each of the four operations accepts three input parameters, and produces one return value. +The `mem*` operations have the following interfaces: +```cpp +void* memcpy( void* dest, const void* src, std::size_t count ); +void* memmove( void* dest, const void* src, std::size_t count ); +void* memset( void* dest, int ch, std::size_t count ); +``` +To deal with only a single interface, this accelerator only provides support for repeating a selection of eight bytes over a desired length `count`, rather than supporting `memset` proper. +The implementation of `memset(dest, ch, count)` can then consist of writing `ch` +for the first $min(8, #`count`)$ bytes, and invoking this ECALL if needed. + +Having settled on the interface for the `mem*` operations, we turn our attention the `write` syscall, which has the following interface#footnote([Linux man-page on `write`; man7.org, version 6.16, 2025-10-29. #link("https://man7.org/linux/man-pages/man2/write.2.html")[[src]]]): +```c +ssize_t write(size_t count; int fd, const void buf[count], size_t count); +``` +To invoke the `write` syscall, one should call `ECALL` with the appropriate syscall number after writing the file descriptor `fd` to `A0` (= `x10`), filling `A1` (= `x11`) with the address of `buf`'s first byte, and making `A2` (= `x12`) contain `count`. +Once the syscall returns, `A0` stores the number of bytes that were written to the `fd` during the syscall. + +Given that this syscall already exists, its interface is fixed and should not be modified: the other operations have to be mapped onto it. +To this end, we require the parameters of the function to be stored in order in `A0`-`A2` before requesting the `ECALL`; this chip ensures the return value is stored in `A0` before handing control back to the `CPU`. + +With all four operations now supplying a `src` and `count` in the same parameter position, reading them from `x11` and `x12` is easily achieved by means of @copy:c:read_src and @copy:c:read_count. +The destination address is found in `x10` for the `mem*` operations; for `write` it is not provided. +To ensure `write` does not overwrite previously written values, register `x254` (initialized to 0), +is used to keep track of the number of bytes previously written. +The value in this register can thus act as the starting point for the `write`-sequence, +as long as it is appropriately updated with each `write` syscall. +Hence, @copy:c:read_dst reads `dst` from either `x10` or `x254` depending on `is_write`, +and overwrites this with the `dst_res`, which is $#`dst` + #`count`$ for `write`-calls (@copy:c:dst_res_is_write) +and just `dst` otherwise (@copy:c:dst_res_non_write). + +What remains is reading `fd` and returning `count` when $#`is_write`=1$, +which is enforced by @copy:c:read_fd. +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]]])), +this constraint enforces that a $1$ is read from `x10`. +Since this chip will always perfectly execute a `write`, this constraint moreover writes `count` as the return value to this register in the same interaction. + +#render_constraint_table(chip, config, groups: "read_input") + +Note: @copy:c:range_dst_res is included to satisfy assumptions made +by the `ADD` template. + + +== Chaining + +Rather than performing the full copy in a single row, this chip splits each operation +in "chunks", with each row in the table representing one such chunk. +Each row copies `step` bytes (which is either $1$ or $8$) from the source to +the destination. +Note that by this model, a copy operation on $x$ bytes can be represented using +$floor.l x / 8 floor.r + x mod 8$ rows. +#footnote[ + The prover is free to select the `step` of each row; an $x$-byte copy could + thus be spread over as many as $x$ rows. + This freedom allows the prover to align the `MEMW` requests, such that they + can be handled by the `MEMW_A` chip, rather than the less efficient `MEMW` chip. +] + +As long as $#`count` > #`step`$, the copy is not done yet, and an extra row +must be introduced. +As such, each row computes an updated `count`, as well as the updated `src` and +`dst` addresses for the bytes that remain to be copied, and forwards this +to the next row using the `COPY_NEXT` interaction @copy:c:send_next_chunk. +The next row then receives this information through @copy:c:receive_next_chunk, +instead of reading this information from the registers as is done on `first`-rows (@reading-parameters). + +#render_constraint_table(chip, config, groups: "forward") + +Note: constraints @copy:c:range_src_incr and @copy:c:range_dst_incr are included to satisfy assumptions made by the `ADD` template; @copy:c:range_count_decr satisfies the assumption made by the `SUB` template (which is inlined through @copy:c:count_borrows). + +== Terminating the recursion + +Observe from @copy:c:send_next_chunk that raising the prover-hinted flag `end` +stops the recursive behaviour. +Without constraining this flag, the prover has two possibilities to cheat: set the +flag early, or set the flag late. +To see how this can be prevented, we first observe that there are two valid states +that should end a sequence: $#`count` = #`step`$ and $(#`count`, #`first`) = (0,1)$. +#footnote[This second case is required to allow a zero-length copy.] +Note that by asserting @copy:c:borrow_implies_first and @copy:c:borrow_implies_count_is_zero, we can use `count_borrows[1]` as proxy to indicate the second state. +The statement $#`end` arrow.double.l.r #`count`=#`step` or (#`count` = 0 and #`first`)$ is then decomposed into +- $#`end` arrow.double.r #`count`=#`step` or (#`count` = 0 and #`first`)$ +- $#`end` arrow.double.l #`count` = #`step`$ +- $#`end` arrow.double.l #`count` = 0 and #`first`$ +where the first implication is captured by constraints +@copy:c:end_implies_count_is_step_or_zc_lower and +@copy:c:end_implies_count_is_step_or_zc_upper, and +the third by @copy:c:borrow_implies_end. +Note that the second implication is already captured indirectly by @copy:c:borrow_implies_first: not setting the flag in this case will lead to a new row with $#`first` = 0$ being introduced (by @copy:c:send_next_chunk) which is guaranteed to have $#`count_borrows[1]` = 1$, thus violating this constraint. + +#render_constraint_table(chip, config, groups: "restrict_end") + +== Performing the move +Constraints @copy:c:read_value and @copy:c:write_value respectively read and write +`value` from/to memory. +Whether eight or just one byte is copied, is determined by the prover-hinted `single` flag. +When set, the top seven bytes in `value` are fixed at zero (@copy:c:single_lanes). + +For most copy operations, the value is read at $#`timestamp`$ and written at $#`timestamp` + 1$. +The exception to this rule, are `memset` operations, performing the write before the read instead. +While this behaviour may seem counterintuitive, this inverse timing technique +ensures the same eight bytes are repeated across the requested memory domain. + +One more requirement for a proper replication, is that $#`dst` = #`src` + 8$, +which is enforced by @copy:c:set_gap. + +#render_constraint_table(chip, config, groups: "copy") + + +== Bits +Lastly, `Bit` variables must be bits, and both `first` and `end` must imply $#`μ` = 1$ to keep the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ binary. +Note that $#`μ` - #`count_borrows[1]`$ is always binary, since $#`count_borrows[1]` => #`μ` = 1$ indirectly holds +via @copy:c:borrow_implies_first. +Additionally, we should make sure that `is_set` and `is_write` do not occur on padding rows, and that `first_write` is correctly defined. +#render_constraint_table(chip, config, groups: ("bits", "functionality")) + += Padding +To pad this chip, use the below data. +#render_chip_padding_table(chip, config) + += The Accelerated Memory Operations standard +This chip is part of the effort to support the Ethereum Foundation's Accelerated +Memory Operations standard. +This standard fixes what an accelerated `memcpy`, `memmove` and `memset` must provide. +#footnote([Accelerated Memory Operations; eth-act/zkevm-standards, commit `a97934c`, 2026-08-11. #link("https://github.com/eth-act/zkevm-standards/blob/a97934cae02693d3b69f07a7cd6e3ed6fb5e8053/standards/accelerated-memory-operations/README.md")[[src]]]) +As requested by the standard, this chip accepts arbitrary operand alignment. + +Note that this chip is only an accelerator; in practice, a library with functions +has to be made to resolve the differences in calling ABI between the +`memset`/`memcpy`/`memmove` functions and the syscalls this chip accelerates. +The `write` interface of this chip corresponds exactly to the syscall ABI, +making it compatible with any normal usage thereof (e.g. by a libc function). + +Moreover, the standard's fourth operation, `memcmp`, is not covered by this chip, as it does not involve copying. +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 +- One could refactor the chip to move sixteen or thirty-two bytes per row instead of eight. + It is suspected that this could be achieved using a 41c/18i and 57c/22i configuration, respectively. +- The chip could be modified to accept the default `memset` interface. diff --git a/spec/meta.typ b/spec/meta.typ index 9e7967c41..6653fb1e3 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -21,7 +21,7 @@ ("is_byte", [`IS_BYTE` template], ), ("is_whh", [`IS_WHH` template], ), ("sign", [`SIGN` template], ), - ("add", [`ADD`/`SUB` template], ), + ("add", [`ADD`/`SUB` templates], ), ("neg", [`NEG` template], ), ("reg", [`REG`/`REGW` template], ), )), @@ -49,11 +49,11 @@ ("ECALLS", ( ("about_ecalls", [About `ECALL`], ), ("halt", [`HALT` chip], ), - ("commit", [`COMMIT` chip], ), ("sha256", [`SHA256` accelerator], ), ("keccak", [`KECCAK` accelerator], ), ("ecsm", [`ECSM` accelerator], ), ("fext", [Extension field accelerator], ), + ("copy", [`COPY` accelerator], ), )), ("RECURSION", ( ("recursion", [Recursive verification], ), diff --git a/spec/src/commit.toml b/spec/src/commit.toml deleted file mode 100644 index f6e77ffd8..000000000 --- a/spec/src/commit.toml +++ /dev/null @@ -1,229 +0,0 @@ -name = "COMMIT" -code = "CMT" - -# Variables - -[[variables.input]] -name = "timestamp" -type = "Word" -desc = "timestamp at which to commit" -pad = 0 - -[[variables.auxiliary]] -name = "index" -type = "BaseField" -desc = "Index of value being committed." -pad = 0 - -[[variables.auxiliary]] -name = "address" -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]] -name = "μ" -type = "Bit" -desc = "" -pad = 0 - -# Assumptions - - -# Constraints - -[[constraint_groups]] -name = "incoming" - -[[constraints.incoming]] -kind = "interaction" -tag = "ECALL" -input = ["timestamp", ["cast", 64, "DWordWL"]] -multiplicity = ["-", "first"] -ref = "commit:c:receive_ecall" - -[[constraint_groups]] -name = "read_input" - -[[constraints.read_input]] -kind = "template" -tag = "REG" -input = [11, "address", "timestamp"] -output = "address" -cond = "first" -ref = "commit:c:read_address" - -[[constraints.read_input]] -kind = "template" -tag = "REG" -input = [12, "count", "timestamp"] -output = "count" -cond = "first" -ref = "commit:c:read_count" - -[[constraints.read_input]] -kind = "template" -tag = "REG" -input = [10, "count", "timestamp"] -output = ["cast", 1, "DWordWL"] -cond = "first" -ref = "commit:c:read_fd_write_count" - -[[constraints.read_input]] -kind = "template" -tag = "REG" -input = [254, ["arr", ["+", "index", ["cast", "count", "BaseField"]], 0], "timestamp"] -output = ["arr", "index", 0] -cond = "first" -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" - -[[constraints.commit]] -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" -multiplicity = "μ" -ref = "commit:c:end" - -[[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/copy.toml b/spec/src/copy.toml new file mode 100644 index 000000000..a92e756b2 --- /dev/null +++ b/spec/src/copy.toml @@ -0,0 +1,407 @@ +name = "COPY" +code = "CPY" + +# Input + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "timestamp at which the operation is requested" +pad = 0 + +# Auxiliary + +[[variables.auxiliary]] +name = "value" +type = "DWordBL" +desc = "The bytes moved by this row; only moves $#`value`_0$ when $#`single` = 1$." +pad = 0 + +[[variables.auxiliary]] +name = "src" +type = "DWordWL" +desc = "Address of the first byte read by this row" +pad = 0 + +[[variables.auxiliary]] +name = "src_incr" +type = "DWordWHH" +desc = "$#`src` + #`step`$" +pad = 8 + +[[variables.auxiliary]] +name = "dst" +type = "DWordWL" +desc = "Address of the first byte written by this row." +pad = 0 + +[[variables.auxiliary]] +name = "dst_incr" +type = "DWordWHH" +desc = "$#`dst` + #`step`$" +pad = 8 + +[[variables.auxiliary]] +name = "count" +type = "DWordWL" +desc = "Number of bytes that still have to be moved, including those moved by this row" +pad = 8 + +[[variables.auxiliary]] +name = "count_decr" +type = "DWordWHH" +desc = "$#`count` - #`step`$" +pad = 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 last row of this sequence" +pad = 0 + +[[variables.auxiliary]] +name = "single" +type = "Bit" +desc = "Whether this row moves a single byte rather than eight" +pad = 0 + +[[variables.auxiliary]] +name = "is_set" +type = "Bit" +desc = "Whether this row is part of a `memset`-sequence" +pad = 0 + +[[variables.auxiliary]] +name = "is_write" +type = "Bit" +desc = "Whether this row is part of a `write`-sequence" +pad = 0 + +[[variables.auxiliary]] +name = "first_write" +type = "Bit" +desc = "$#`first` dot #`is_write`$; whether this row is the first of a `write` sequence" +pad = 0 + +[[variables.auxiliary]] +name = "dst_res" +type = "DWordWHH" +desc = "$#`dst` + #`count` dot #`is_write`$" +pad = 0 + +# Virtual + +[[variables.virtual]] +name = "step" +type = "Byte" +desc = "The stride this row advances by: $1$ if `single` is set, or $8$ otherwise." +def = ["-", 8, ["*", 7, "single"]] + +[[variables.virtual]] +name = "count_borrows" +desc = "Borrow values used to constrain $#`count_decr` = #`count` - #`step`$." +type = ["Bit", 2] +def = {idx="i", polys=[ + {iter=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "count_decr", "DWordWL"], 0], "step"], ["idx", "count", 0]]]}, + {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "count_decr", "DWordWL"], 1], ["idx", "count_borrows", 0]], ["idx", "count", 1]]]}, +]} + +# Multiplicity + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +# Assumptions + +[[assumptions]] +desc = "`IS_WORD[timestamp]`" +ref = "copy:a:timestamp" + +[[assumptions]] +desc = "`IS_WORD[src[i]]`" +iter = ["i", 0, 1] +ref = "copy:a:src" + +[[assumptions]] +desc = "`IS_WORD[dst[i]]`" +iter = ["i", 0, 1] +ref = "copy:a:dst" + +[[assumptions]] +desc = "`IS_WORD[count[i]]`" +iter = ["i", 0, 1] +ref = "copy:a:count" + +# Constraints + +[[constraint_groups]] +name = "ecall" + +[[constraints.ecall]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["+", 64, ["*", ["-", ["^", 2, 32], 94], ["-", 1, "is_write"]]], "is_set"], ["*", ["-", ["^", 2, 32], 1], ["-", 1, "is_write"]]]] +multiplicity = ["-", "first"] +ref = "copy:c:receive_ecall" + +[[constraint_groups]] +name = "flags" + +[[constraints.flags]] +kind = "template" +tag = "IS_BIT" +input = ["is_set"] +ref = "copy:c:range_is_set" + +[[constraints.flags]] +kind = "template" +tag = "IS_BIT" +input = ["is_write"] +ref = "copy:c:range_is_write" + +[[constraints.flags]] +kind = "arith" +constraint = "$#`is_set` dot #`is_write` = 0$" +poly = ["*", "is_set", "is_write"] +ref = "copy:c:one_hot" + +[[constraint_groups]] +name = "functionality" + +[[constraints.functionality]] +kind = "arith" +constraint = "$#`is_set` + #`is_write` => #`μ` = 1$" +poly = ["*", ["+", "is_set", "is_write"], ["not", "μ"]] +ref = "copy:c:functionality_implies_mu" + +[[constraints.functionality]] +kind = "arith" +constraint = "$#`first_write` = #`first` dot #`is_write`$" +poly = ["-", "first_write", ["*", "first", "is_write"]] +ref = "copy:c:first_write" + +[[constraint_groups]] +name = "read_input" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [11, "src", "timestamp"] +output = "src" +cond = "first" +ref = "copy:c:read_src" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [12, "count", "timestamp"] +output = "count" +cond = "first" +ref = "copy:c:read_count" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [["+", 10, ["*", 244, "is_write"]], ["cast", "dst_res", "DWordWL"], "timestamp"] +output = "dst" +cond = "first" +ref = "copy:c:read_dst" + +[[constraints.read_input]] +kind = "template" +tag = "ADD" +input = ["dst", "count"] +output = ["cast", "dst_res", "DWordWL"] +cond = "is_write" +ref = "copy:c:dst_res_is_write" + +[[constraints.read_input]] +kind = "arith" +constraint = "$!#`is_write` => #`dst_res` = #`dst`$" +poly = ["*", ["not", "is_write"], ["-", ["idx", ["cast", "dst_res", "DWordWL"], "i"], ["idx", "dst", "i"]]] +iter = ["i", 0, 1] +ref = "copy:c:dst_res_non_write" + +[[constraints.read_input]] +kind = "template" +tag = "IS_WHH" +input = ["dst_res"] +cond = "is_write" +ref = "copy:c:range_dst_res" + +[[constraints.read_input]] +kind = "template" +tag = "REG" +input = [10, "count", "timestamp"] +output = ["cast", 1, "DWordWL"] +cond = "first_write" +ref = "copy:c:read_fd" + +[[constraint_groups]] +name = "forward" + +[[constraints.forward]] +kind = "template" +tag = "ADD" +input = [["cast", "src", "DWordWL"], ["arr", "step", 0]] +output = ["cast", "src_incr", "DWordWL"] +ref = "copy:c:src_incr" + +[[constraints.forward]] +kind = "template" +tag = "ADD" +input = [["cast", "dst", "DWordWL"], ["arr", "step", 0]] +output = ["cast", "dst_incr", "DWordWL"] +ref = "copy:c:dst_incr" + +[[constraints.forward]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "count_borrows", "i"]] +iter = ["i", 0, 1] +ref = "copy:c:count_borrows" + +[[constraints.forward]] +kind = "template" +tag = "IS_WHH" +input = ["src_incr"] +cond = "μ" +ref = "copy:c:range_src_incr" + +[[constraints.forward]] +kind = "template" +tag = "IS_WHH" +input = ["dst_incr"] +cond = "μ" +ref = "copy:c:range_dst_incr" + +[[constraints.forward]] +kind = "template" +tag = "IS_WHH" +input = ["count_decr"] +cond = "μ" +ref = "copy:c:range_count_decr" + +[[constraints.forward]] +kind = "interaction" +tag = "COPY_NEXT" +input = ["timestamp", ["cast", "src_incr", "DWordWL"], ["cast", "dst_incr", "DWordWL"], ["cast", "count_decr", "DWordWL"], "is_set", "is_write"] +multiplicity = ["-", "μ", "end"] +ref = "copy:c:send_next_chunk" + +[[constraints.forward]] +kind = "interaction" +tag = "COPY_NEXT" +input = ["timestamp", "src", "dst", "count", "is_set", "is_write"] +multiplicity = ["-", ["-", "μ", "first"]] +ref = "copy:c:receive_next_chunk" + +[[constraint_groups]] +name = "restrict_end" + +[[constraints.restrict_end]] +kind = "arith" +constraint = "$#`count_borrows[1]` => #`first`$" +poly = ["*", ["idx", "count_borrows", 1], ["not", "first"]] +ref = "copy:c:borrow_implies_first" + +[[constraints.restrict_end]] +kind = "arith" +constraint = "$#`count_borrows[1]` => #`count` = 0$" +poly = ["*", ["idx", "count_borrows", 1], ["idx", "count", "i"]] +iter = ["i", 0, 1] +ref = "copy:c:borrow_implies_count_is_zero" + +[[constraints.restrict_end]] +kind = "arith" +constraint = "$#`end` => #`count_borrows[1]` or floor.l #`count` / 2^32 floor.r = 0$" +poly = ["*", "end", ["not", ["idx", "count_borrows", 1]], ["idx", "count", 1]] +ref = "copy:c:end_implies_count_is_step_or_zc_upper" + +[[constraints.restrict_end]] +kind = "arith" +constraint = "$#`end` => #`count_borrows[1]` or #`count[0]` = #`step`$" +poly = ["*", "end", ["not", ["idx", "count_borrows", 1]], ["-", ["idx", "count", 0], "step"]] +ref = "copy:c:end_implies_count_is_step_or_zc_lower" + +[[constraints.restrict_end]] +kind = "arith" +constraint = "$#`count_borrows[1]` => #`end`$" +poly = ["*", ["idx", "count_borrows", 1], ["not", "end"]] +ref = "copy:c:borrow_implies_end" + +[[constraint_groups]] +name = "copy" + +[[constraints.copy]] +kind = "interaction" +tag = "MEMW" +input = [0, "src", "value", ["+", "timestamp", "is_set"], 0, 0, ["not", "single"]] +output = "value" +multiplicity = ["-", "μ", ["idx", "count_borrows", 1]] +ref = "copy:c:read_value" + +[[constraints.copy]] +kind = "interaction" +tag = "MEMW" +input = [["*", 2, "is_write"], "dst", "value", ["+", "timestamp", ["-", 1, "is_set"]], 0, 0, ["not", "single"]] +multiplicity = ["-", "μ", ["idx", "count_borrows", 1]] +ref = "copy:c:write_value" + +[[constraints.copy]] +kind = "arith" +constraint = "$#`single` => #`value`_i = 0$" +poly = ["*", "single", ["idx", "value", "i"]] +iter = ["i", 1, 7] +ref = "copy:c:single_lanes" + +[[constraints.copy]] +kind = "template" +tag = "ADD" +input = ["src", ["arr", 8, 0]] +output = "dst" +cond = "is_set" +ref = "copy:c:set_gap" + +[[constraint_groups]] +name = "bits" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["first"] +ref = "copy:c:range_first" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["end"] +ref = "copy:c:range_end" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["single"] +ref = "copy:c:range_single" + +[[constraints.bits]] +kind = "template" +tag = "IS_BIT" +input = ["μ"] +ref = "copy:c:range_mu" + +[[constraints.bits]] +kind = "arith" +constraint = "$#`first` + #`end` => #`μ` = 1$" +poly = ["*", ["+", "first", "end"], ["not", "μ"]] +ref = "copy:c:first_or_end_implies_mu" + diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index df80e21cb..73e6c9a5d 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -118,11 +118,11 @@ tag = "ECALL" kind = "interaction" input = ["Word", "DWordWL"] -# CNB[timestamp, index, address, count] +# COPY_NEXT[timestamp, src, dst, count, is_set, is_write] [[signatures]] -tag = "CNB" +tag = "COPY_NEXT" kind = "interaction" -input = ["Word", "BaseField", "DWordWL", "DWordWL"] +input = ["Word", "DWordWL", "DWordWL", "DWordWL", "Bit", "Bit"] # BYTE_ALU[res; selector, X, Y] [[signatures]] @@ -164,6 +164,13 @@ tag = "IS_HALF" kind = "interaction" input = ["Half"] +# IS_WHH[X] +[[signatures]] +tag = "IS_WHH" +kind = "template" +input = ["DWordWHH"] +cond = "BaseField" + # IS_B20[X] [[signatures]] tag = "IS_B20" @@ -176,13 +183,6 @@ tag = "IS_WH" kind = "interaction" input = ["Word", "Half"] -# IS_WHH[X, Y] -[[signatures]] -tag = "IS_WHH" -kind = "template" -input = ["DWordWHH"] -cond = "BaseField" - # HWSL[res; X, shift] [[signatures]] tag = "HWSL"