diff --git a/spec/book.typ b/spec/book.typ index 076d31cf3..7a55323cd 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -33,6 +33,11 @@ summary: meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join() ) +#let common-formatting(body) = { + set footnote(numbering: "[1]") + body +} + #let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[ #set text(fill: foreground) @@ -134,6 +139,7 @@ assert(meta.summary.find(((f, _, _)) => f == file) != none, message: "Couldn't resolve typst source file " + file) if is-shiroa { (body) => { + show: common-formatting context _xref-included.update(x => x + ((file): true)) context _toplevel.update(s => { if s == none { @@ -151,6 +157,6 @@ ]) } } else { - (body) => body + body => body } } diff --git a/spec/ebook.typ b/spec/ebook.typ index f9ba76046..e1b15253e 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -1,4 +1,4 @@ -#import "/book.typ": style, meta +#import "/book.typ": style, meta, common-formatting #set document(author: meta.authors, title: meta.title) @@ -10,6 +10,7 @@ #pagebreak(weak: true) #outline() +#show: common-formatting #show heading: set heading(numbering: "1.1") #meta.summary.map(((ch, title, ref)) => [ diff --git a/spec/ecall.typ b/spec/ecall.typ index 6908f768b..dd3544ef3 100644 --- a/spec/ecall.typ +++ b/spec/ecall.typ @@ -12,6 +12,15 @@ #let config = load_config() #show: book-page("ecall.typ") += About `ECALL` +When `ECALL` is executed, it is assumed that: +- register `A7` contains the system call number + #footnote([The RISC-V system call ABI; libriscv.no, #link("https://web.archive.org/web/20260128152107/https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[src]]]), +- the arguments are located in registers `A0`-`A6`, and +- the return value is written to `A0`, +where `A0`-`A7` are symbolic names for the registers `x10`-`x17` +#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]). + #let config = load_config() #let chip = load_chip("src/halt.toml", config) @@ -45,13 +54,113 @@ This prevents any other operation involving memory from being executed hereafter ]) === Lookup -The HALT chip contributes the following interaction to the lookup-argument: +In this VM, halting is considered equivalent to executing a `sys_exit`. +Hence, this chip responds to `ECALL`s with system call number 93. +#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#L258")[[src]]]) +The HALT chip therefore contributes the following interaction to the lookup-argument: #render_constraint_table(chip, config, groups: "lookup") -*Note*: #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/linux-headers/include/asm-generic/unistd.h#L258")[$93$ is the system call number corresponding to `sys_exit`.] - == Padding This chip should only contain a single row. Given that $2^0 = 1$, this chip does not need to be padded. As such, no padding is defined. + +#let config = load_config() +#let chip = load_chip("src/commit.toml", config) +#let commit = raw(chip.name) += #commit chip + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #commit chip leverages #nr_variables variables, spanning #nr_columns columns: +#render_chip_column_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]]]) +#[ +#show raw.where(block: true): it => block(it, fill: luma(230), inset: 1em, width: 100%, radius: 5pt) +```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. +#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 @add:a:rhs. +#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/src/commit.toml b/spec/src/commit.toml new file mode 100644 index 000000000..5d8325363 --- /dev/null +++ b/spec/src/commit.toml @@ -0,0 +1,221 @@ +name = "COMMIT" + +# Variables + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +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 = ["arr", 0, 0, 0, 0] + +[[variables.auxiliary]] +name = "address_incr" +type = "DWordHL" +desc = "$#`address` + 1$" +pad = ["arr", 1, 0, 0, 0] + +[[variables.auxiliary]] +name = "count" +type = "DWordWL" +desc = "number of bytes to commit" +pad = ["arr", 1, 0, 0, 0] + +[[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",64] +multiplicity = ["-", "first"] +ref = "commit:c:receive_ecall" + +[[constraint_groups]] +name = "read_input" + +[[constraints.read_input]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, 11], "address", "timestamp", 1, 0, 0] +output = "address" +multiplicity = "first" +ref = "commit:c:read_address" + +[[constraints.read_input]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, 12], "count", "timestamp", 1, 0, 0] +output = "count" +multiplicity = "first" +ref = "commit:c:read_count" + +[[constraints.read_input]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, 10], "count", "timestamp", 1, 0, 0] +output = 1 +multiplicity = "first" +ref = "commit:c:read_fd_write_count" + +[[constraints.read_input]] +kind = "interaction" +tag = "MEMW" +input = [1, ["*", 2, 254], ["+", "index", ["cast", "count", "BaseField"]], "timestamp", 0, 0, 0] +output = "index" +multiplicity = "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 = "MEWM" +input = [0, "address", "value", "timestamp", 0, 0, 0] +output = "value" +multiplicity = ["-", "μ", "end"] +ref = "commit:c:read_value" + +[[constraints.commit]] +kind = "interaction" +tag = "COMMIT" +input = ["index", "value"] +multiplicity = ["-", "μ", "end"] +ref = "commit:c:commit_value" + +[[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"], "count_decr"] +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"