spec: COMMIT chip

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
   }
 }

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)) => [

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.

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"