From 414d5ef9f298df77d8a03765830b82b514998286 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Wed, 4 Feb 2026 11:20:59 +0100
Subject: [PATCH 01/12] spec: update footnote numbering

---
 spec/ebook.typ | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/spec/ebook.typ b/spec/ebook.typ
index f9ba76046..dd53084e7 100644
--- a/spec/ebook.typ
+++ b/spec/ebook.typ
@@ -6,6 +6,8 @@
   foreground: black,
 ))
 
+#set footnote(numbering: "[1]")
+
 #align(center, title(meta.title))
 #pagebreak(weak: true)
 #outline()

From 3e130d3b1446d20f7839918fd30b8b4fdf94319a Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Wed, 4 Feb 2026 12:18:58 +0100
Subject: [PATCH 02/12] spec: COMMIT: specify commit chip

---
 spec/ecall.typ       |  78 ++++++++++++++++
 spec/src/commit.toml | 210 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 288 insertions(+)
 create mode 100644 spec/src/commit.toml

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 6908f768b..68c4914b5 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(link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[The RISC-V system call ABI; libriscv.no. Accessed Feb 4, 2026.]),
+- 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(link("https://en.wikipedia.org/wiki/RISC-V#Register_sets")[RISC-V - Register sets; en.wikipedia.org. Accessed on Feb 4, 2026.]).
+
 
 #let config = load_config()
 #let chip = load_chip("src/halt.toml", config)
@@ -55,3 +64,72 @@ 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([$64$ is the system call number corresponding to `sys_write`. #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/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 "call" 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")
+*Note*: the prover is free to specify the value of `first` as they see fit; @commit:c:range_first only makes sure it must be a `Bit`.
+Also, `first` being set must imply that that this is not a padding row (@commit:c:first_implies_mu).
+
+The `write` operation --- writing to a file descriptor --- has the following signature:
+#footnote([Linux man-page on `write`; man7.org, #link("https://man7.org/linux/man-pages/man2/write.2.html")[[src]]. Accessed Feb 4, 2026.])
+#[
+#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`.
+
+Since we only support writing to `stdout` (which corresponds to $#`fd` = 1$
+#footnote([The Open Group Base Specifications, `unistd.h`; The Open Group, issue 7, #link("https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/unistd.h.html")[[src]]. Accessed Feb 4, 2026.]))
+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 multiple for a commit to be interrupted or fail.
+Furthermore, @commit:c:read_address reads `address` from `x11` and @commit:c:read_count reads `count` from `x12`.
+Again, these memory interactions only take place when this is the `first` call in the recursion tree.
+#render_constraint_table(chip, config, groups: "read_input")
+
+Next, we read the `value` located at buffer address `address` and commit to it:
+#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.
+@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_decr` (the number of bytes still to be committed) hits $0$, we should stop recursing.
+To this end, `last` is set this is the case (@commit:c:last).
+To prevent undesired lookups from occurring, `last` should only be set when we're not padding (@commit:c:last_implies_mu).
+Also, we must make sure `mu` is a bit (@commit:c:range_mu).
+#render_constraint_table(chip, config, groups: "last")
+
+Lastly, when this was not the `last` 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")
+
+== Padding
+To pad this chip, use the below data.
+This corresponds to committing a $0$ from address $0$.
+#render_chip_padding_table(chip, config)
diff --git a/spec/src/commit.toml b/spec/src/commit.toml
new file mode 100644
index 000000000..17e400f5c
--- /dev/null
+++ b/spec/src/commit.toml
@@ -0,0 +1,210 @@
+name = "COMMIT"
+
+# Variables
+
+[[variables.input]]
+name = "index"
+type = "RowIndex"
+desc = "index of value being committed"
+precomputed = 1
+
+[[variables.input]]
+name = "timestamp"
+type = "DWordWL"
+desc = "timestamp at which to commit"
+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 write to commit"
+pad = 1
+
+[[variables.auxiliary]]
+name = "count_decr"
+type = "DWordHL"
+desc = "$#`count` - 1$"
+pad = 0
+
+[[variables.auxiliary]]
+name = "first"
+type = "Bit"
+desc = "Whether this is the first commitment in this sequence."
+pad = 0
+
+[[variables.auxiliary]]
+name = "last"
+type = "Bit"
+desc = "Whether this is the last commitment in this 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"
+
+[[constraints.incoming]]
+kind = "template"
+tag = "IS_BIT"
+input = ["first"]
+ref = "commit:c:range_first"
+
+[[constraints.incoming]]
+kind = "arith"
+constraint = "$#`first` => #`μ` = 1$"
+poly = ["*", "first", ["not", "μ"]]
+ref = "commit:c:first_implies_mu"
+
+[[constraint_groups]]
+name = "read_input"
+
+[[constraints.read_input]]
+kind = "interaction"
+tag = "MEMW"
+input = [1, 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, 11, "address", "timestamp", 1, 0, 0]
+output = "address"
+multiplicity = "first"
+ref = "commit:c:read_address"
+
+[[constraints.read_input]]
+kind = "interaction"
+tag = "MEMW"
+input = [1, 12, "count", "timestamp", 1, 0, 0]
+output = "count"
+multiplicity = "first"
+ref = "commit:c:read_count"
+
+
+[[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 = "μ"
+ref = "commit:c:read_value"
+
+[[constraints.commit]]
+kind = "interaction"
+tag = "COMMIT"
+input = ["index", "value"]
+multiplicity = "μ"
+ref = "commit:c:commit_value"
+
+[[constraint_groups]]
+name = "last"
+
+[[constraints.last]]
+kind = "interaction"
+tag = "ZERO"
+input = [["+", ["idx", "count_decr", 0], ["idx", "count_decr", 1], ["idx", "count_decr", 2], ["idx", "count_decr", 3]]]
+output = "last"
+multiplicity = "μ"
+ref = "commit:c:last"
+
+[[constraints.last]]
+kind = "arith"
+constraint = "$#`last` => #`μ` = 1$"
+poly = ["*", "last", ["not", "μ"]]
+ref = "commit:c:last_implies_mu"
+
+[[constraints.last]]
+kind = "template"
+tag = "IS_BIT"
+input = ["μ"]
+ref = "commit:c:range_mu"
+
+[[constraint_groups]]
+name = "lookups"
+
+[[constraints.lookups]]
+kind = "interaction"
+tag = "CNB"
+input = ["timestamp", "address_incr", "count_decr"]
+multiplicity = ["-", "μ", "last"]
+ref = "commit:c:send_commit_next_byte"
+
+[[constraints.lookups]]
+kind = "interaction"
+tag = "CNB"
+input = ["timestamp", "address", "count"]
+multiplicity = ["-", "first", "μ"]
+ref = "commit:c:receive_commit_next_byte"

From 275ed8b67dd0fb8a9a9e863a90d54eaee2fabea7 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Thu, 5 Feb 2026 10:36:35 +0100
Subject: [PATCH 03/12] spec: COMMIT: fix typos

---
 spec/ecall.typ | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 68c4914b5..64f31a5d6 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -107,7 +107,7 @@ Since we only support writing to `stdout` (which corresponds to $#`fd` = 1$
 #footnote([The Open Group Base Specifications, `unistd.h`; The Open Group, issue 7, #link("https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/unistd.h.html")[[src]]. Accessed Feb 4, 2026.]))
 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 multiple for a commit to be interrupted or fail.
+in this VM it is impossible for a commit to be interrupted or fail.
 Furthermore, @commit:c:read_address reads `address` from `x11` and @commit:c:read_count reads `count` from `x12`.
 Again, these memory interactions only take place when this is the `first` call in the recursion tree.
 #render_constraint_table(chip, config, groups: "read_input")
@@ -120,7 +120,7 @@ In parallel, we compute $#`address_incr` = #`address` + 1$ (@commit:c:address_in
 #render_constraint_table(chip, config, groups: "incr_decr")
 
 When `count_decr` (the number of bytes still to be committed) hits $0$, we should stop recursing.
-To this end, `last` is set this is the case (@commit:c:last).
+To this end, `last` is set when this is the case (@commit:c:last).
 To prevent undesired lookups from occurring, `last` should only be set when we're not padding (@commit:c:last_implies_mu).
 Also, we must make sure `mu` is a bit (@commit:c:range_mu).
 #render_constraint_table(chip, config, groups: "last")

From 45af27e924f056ce1d8ae5a90abec50ef9ddaeb7 Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Thu, 5 Feb 2026 11:24:40 +0100
Subject: [PATCH 04/12] Move footnote numbering to a more general spot and
 allow easy future updates

---
 spec/book.typ  | 8 +++++++-
 spec/ebook.typ | 2 --
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/spec/book.typ b/spec/book.typ
index 076d31cf3..2b2f8dee1 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
+    common-formatting
   }
 }
diff --git a/spec/ebook.typ b/spec/ebook.typ
index dd53084e7..f9ba76046 100644
--- a/spec/ebook.typ
+++ b/spec/ebook.typ
@@ -6,8 +6,6 @@
   foreground: black,
 ))
 
-#set footnote(numbering: "[1]")
-
 #align(center, title(meta.title))
 #pagebreak(weak: true)
 #outline()

From b18b7618604a13a3172f58c93109902597317d8f Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Fri, 6 Feb 2026 13:26:38 +0100
Subject: [PATCH 05/12] Update common-formatting location

---
 spec/book.typ  | 2 +-
 spec/ebook.typ | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/spec/book.typ b/spec/book.typ
index 2b2f8dee1..7a55323cd 100644
--- a/spec/book.typ
+++ b/spec/book.typ
@@ -157,6 +157,6 @@
       ])
     }
   } else {
-    common-formatting
+    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)) => [

From 48220a80f22c9445fbbdbaaa1e064b7a2c899bd8 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 10 Feb 2026 10:16:12 +0100
Subject: [PATCH 06/12] spec: COMMIT: update citation links

---
 spec/ecall.typ | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 64f31a5d6..11c5b0963 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -15,11 +15,11 @@
 = About `ECALL`
 When `ECALL` is executed, it is assumed that:
 - register `A7` contains the system call number
-  #footnote(link("https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[The RISC-V system call ABI; libriscv.no. Accessed Feb 4, 2026.]),
+  #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(link("https://en.wikipedia.org/wiki/RISC-V#Register_sets")[RISC-V - Register sets; en.wikipedia.org. Accessed on Feb 4, 2026.]).
+#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()
@@ -54,11 +54,12 @@ 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.
@@ -80,7 +81,7 @@ The #commit chip leverages #nr_variables variables, spanning #nr_columns columns
 == 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([$64$ is the system call number corresponding to `sys_write`. #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/master/linux-headers/include/asm-generic/unistd.h#L174")[[src]]])
+#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 "call" 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.
@@ -90,7 +91,7 @@ This is why @commit:c:receive_ecall has multiplicity $-#`first`$.
 Also, `first` being set must imply that that this is not a padding row (@commit:c:first_implies_mu).
 
 The `write` operation --- writing to a file descriptor --- has the following signature:
-#footnote([Linux man-page on `write`; man7.org, #link("https://man7.org/linux/man-pages/man2/write.2.html")[[src]]. Accessed Feb 4, 2026.])
+#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
@@ -104,7 +105,7 @@ That is to say,
 - the written count should be written to `A0`.
 
 Since we only support writing to `stdout` (which corresponds to $#`fd` = 1$
-#footnote([The Open Group Base Specifications, `unistd.h`; The Open Group, issue 7, #link("https://pubs.opengroup.org/onlinepubs/9699919799/basedefs/unistd.h.html")[[src]]. Accessed Feb 4, 2026.]))
+#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.

From 49831de8697d6925006f02a9c0da548738177caa Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 10 Feb 2026 12:20:24 +0100
Subject: [PATCH 07/12] spec: COMMIT: deal with committing 0 bytes

---
 spec/ecall.typ       |  46 ++++++++++++------
 spec/src/commit.toml | 109 ++++++++++++++++++++++++-------------------
 2 files changed, 93 insertions(+), 62 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 11c5b0963..51a235962 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -83,12 +83,10 @@ 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 "call" itself to commit the remaining bytes.
+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")
-*Note*: the prover is free to specify the value of `first` as they see fit; @commit:c:range_first only makes sure it must be a `Bit`.
-Also, `first` being set must imply that that this is not a padding row (@commit:c:first_implies_mu).
 
 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]]])
@@ -104,33 +102,53 @@ That is to say,
 - `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.
-Furthermore, @commit:c:read_address reads `address` from `x11` and @commit:c:read_count reads `count` from `x12`.
-Again, these memory interactions only take place when this is the `first` call in the recursion tree.
+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")
 
-Next, we read the `value` located at buffer address `address` and commit to it:
+*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.
+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.
+Both of these constraints are only required when $#`μ` = 1$, to permit a simpler padding configuration.
 @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_decr` (the number of bytes still to be committed) hits $0$, we should stop recursing.
-To this end, `last` is set when this is the case (@commit:c:last).
-To prevent undesired lookups from occurring, `last` should only be set when we're not padding (@commit:c:last_implies_mu).
-Also, we must make sure `mu` is a bit (@commit:c:range_mu).
-#render_constraint_table(chip, config, groups: "last")
+When `count` hits $0$, we should performing further recursive calls.
+We use the `end` bit to indicate these circumstances.
+
+#render_constraint_table(chip, config, groups: "end")
 
-Lastly, when this was not the `last` 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).
+*Note*: 
++ Rather than setting $#`end` = 1$ when $#`count` = 0$, we do so $#`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.
-This corresponds to committing a $0$ from address $0$.
 #render_chip_padding_table(chip, config)
diff --git a/spec/src/commit.toml b/spec/src/commit.toml
index 17e400f5c..89c65c54c 100644
--- a/spec/src/commit.toml
+++ b/spec/src/commit.toml
@@ -2,18 +2,18 @@ name = "COMMIT"
 
 # Variables
 
-[[variables.input]]
-name = "index"
-type = "RowIndex"
-desc = "index of value being committed"
-precomputed = 1
-
 [[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"
@@ -24,13 +24,13 @@ pad = 0
 name = "address_incr"
 type = "DWordHL"
 desc = "$#`address` + 1$"
-pad = 1
+pad = 0
 
 [[variables.auxiliary]]
 name = "count"
 type = "DWordWL"
-desc = "number of bytes to write to commit"
-pad = 1
+desc = "number of bytes to commit"
+pad = 0
 
 [[variables.auxiliary]]
 name = "count_decr"
@@ -45,9 +45,9 @@ desc = "Whether this is the first commitment in this sequence."
 pad = 0
 
 [[variables.auxiliary]]
-name = "last"
+name = "end"
 type = "Bit"
-desc = "Whether this is the last commitment in this sequence."
+desc = "Whether this is the end of the commitment sequence."
 pad = 0
 
 [[variables.auxiliary]]
@@ -77,44 +77,40 @@ input = ["timestamp",64]
 multiplicity = ["-", "first"]
 ref = "commit:c:receive_ecall"
 
-[[constraints.incoming]]
-kind = "template"
-tag = "IS_BIT"
-input = ["first"]
-ref = "commit:c:range_first"
-
-[[constraints.incoming]]
-kind = "arith"
-constraint = "$#`first` => #`μ` = 1$"
-poly = ["*", "first", ["not", "μ"]]
-ref = "commit:c:first_implies_mu"
-
 [[constraint_groups]]
 name = "read_input"
 
 [[constraints.read_input]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, 10, "count", "timestamp", 1, 0, 0]
-output = 1
+input = [1, ["*", 2, 11], "address", "timestamp", 1, 0, 0]
+output = "address"
 multiplicity = "first"
-ref = "commit:c:read_fd_write_count"
+ref = "commit:c:read_address"
 
 [[constraints.read_input]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, 11, "address", "timestamp", 1, 0, 0]
-output = "address"
+input = [1, ["*", 2, 12], "count", "timestamp", 1, 0, 0]
+output = "count"
 multiplicity = "first"
-ref = "commit:c:read_address"
+ref = "commit:c:read_count"
 
 [[constraints.read_input]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, 12, "count", "timestamp", 1, 0, 0]
-output = "count"
+input = [1, ["*", 2, 10], "count", "timestamp", 1, 0, 0]
+output = 1
 multiplicity = "first"
-ref = "commit:c:read_count"
+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]]
@@ -125,6 +121,7 @@ kind = "template"
 tag = "ADD"
 input = ["address", ["cast", 1, "DWordWL"]]
 output = ["cast", "address_incr", "DWordWL"]
+cond = "μ"
 ref = "commit:c:address_incr"
 
 [[constraints.incr_decr]]
@@ -140,6 +137,7 @@ kind = "template"
 tag = "SUB"
 input = ["count", ["cast", 1, "DWordWL"]]
 output = ["cast", "count_decr", "DWordWL"]
+cond = "μ"
 ref = "commit:c:count_decr"
 
 [[constraints.incr_decr]]
@@ -159,52 +157,67 @@ kind = "interaction"
 tag = "MEWM"
 input = [0, "address", "value", "timestamp", 0, 0, 0]
 output = "value"
-multiplicity = "μ"
+multiplicity = ["-", "μ", "end"]
 ref = "commit:c:read_value"
 
 [[constraints.commit]]
 kind = "interaction"
 tag = "COMMIT"
 input = ["index", "value"]
-multiplicity = "μ"
+multiplicity = ["-", "μ", "end"]
 ref = "commit:c:commit_value"
 
 [[constraint_groups]]
-name = "last"
+name = "end"
 
-[[constraints.last]]
+[[constraints.end]]
 kind = "interaction"
 tag = "ZERO"
-input = [["+", ["idx", "count_decr", 0], ["idx", "count_decr", 1], ["idx", "count_decr", 2], ["idx", "count_decr", 3]]]
-output = "last"
+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:last"
+ref = "commit:c:end"
 
-[[constraints.last]]
-kind = "arith"
-constraint = "$#`last` => #`μ` = 1$"
-poly = ["*", "last", ["not", "μ"]]
-ref = "commit:c:last_implies_mu"
+[[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.last]]
+[[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", "address_incr", "count_decr"]
-multiplicity = ["-", "μ", "last"]
+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", "address", "count"]
+input = ["timestamp", "index", "address", "count"]
 multiplicity = ["-", "first", "μ"]
 ref = "commit:c:receive_commit_next_byte"

From 99c1cffab0507bb27d3117b5bc5df9e50cc303f3 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 10 Feb 2026 12:22:05 +0100
Subject: [PATCH 08/12] spec: COMMIT: list future improvement

---
 spec/ecall.typ | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 51a235962..c156aabe5 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -152,3 +152,7 @@ These are required to ensure the multiplicities $#`first` - #`μ`$ and $#`μ` -
 == Padding
 To pad this chip, use the below data.
 #render_chip_padding_table(chip, config)
+
+== Notes
+- The current version only supports writing to `stdout`.
+  This chip could potentially be extended to support writing to arbitrary `fd`s

From 90211883dfc22ef794d5ccbebcf2631ce7a4681a Mon Sep 17 00:00:00 2001
From: Erik <159244975+erik-3milabs@users.noreply.github.com>
Date: Wed, 11 Feb 2026 09:55:30 +0100
Subject: [PATCH 09/12] Fix typos

Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech>
---
 spec/ecall.typ | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index c156aabe5..0d073ec11 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -127,13 +127,13 @@ Both of these constraints are only required when $#`μ` = 1$, to permit a simple
 @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 performing further recursive calls.
+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 $#`count_decr` = -1$.
++ 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, 

From aeeddaeb5bf1d146575a3bbcbbc6029b66abb3a8 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Wed, 11 Feb 2026 09:57:48 +0100
Subject: [PATCH 10/12] spec: COMMIT: rearrange CNB multiplicity

---
 spec/ecall.typ       | 2 +-
 spec/src/commit.toml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 0d073ec11..8f9296795 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -146,7 +146,7 @@ Since that certainly won't be the `first` call in the sequence, we read `address
 #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.
+These are required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary.
 #render_constraint_table(chip, config, groups: "bits")
 
 == Padding
diff --git a/spec/src/commit.toml b/spec/src/commit.toml
index 89c65c54c..50875b024 100644
--- a/spec/src/commit.toml
+++ b/spec/src/commit.toml
@@ -219,5 +219,5 @@ ref = "commit:c:send_commit_next_byte"
 kind = "interaction"
 tag = "CNB"
 input = ["timestamp", "index", "address", "count"]
-multiplicity = ["-", "first", "μ"]
+multiplicity = ["-", ["-", "μ", "first"]]
 ref = "commit:c:receive_commit_next_byte"

From 61b00aa1470bfea9eee757dec1fdce98f2328199 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Wed, 11 Feb 2026 10:16:23 +0100
Subject: [PATCH 11/12] spec: COMMIT: update padding strategy permitting ADD
 and SUB constraints of lower degree

---
 spec/ecall.typ       |  1 -
 spec/src/commit.toml | 10 ++++------
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 8f9296795..62539fa67 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -123,7 +123,6 @@ This is only performed when we have not yet reached the `end` of the commit sequ
 #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.
-Both of these constraints are only required when $#`μ` = 1$, to permit a simpler padding configuration.
 @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")
 
diff --git a/spec/src/commit.toml b/spec/src/commit.toml
index 50875b024..5d8325363 100644
--- a/spec/src/commit.toml
+++ b/spec/src/commit.toml
@@ -18,25 +18,25 @@ pad = 0
 name = "address"
 type = "DWordWL"
 desc = "Address of first byte to commit."
-pad = 0
+pad = ["arr", 0, 0, 0, 0]
 
 [[variables.auxiliary]]
 name = "address_incr"
 type = "DWordHL"
 desc = "$#`address` + 1$"
-pad = 0
+pad = ["arr", 1, 0, 0, 0]
 
 [[variables.auxiliary]]
 name = "count"
 type = "DWordWL"
 desc = "number of bytes to commit"
-pad = 0
+pad = ["arr", 1, 0, 0, 0]
 
 [[variables.auxiliary]]
 name = "count_decr"
 type = "DWordHL"
 desc = "$#`count` - 1$"
-pad = 0
+pad = ["arr", 0, 0, 0, 0]
 
 [[variables.auxiliary]]
 name = "first"
@@ -121,7 +121,6 @@ kind = "template"
 tag = "ADD"
 input = ["address", ["cast", 1, "DWordWL"]]
 output = ["cast", "address_incr", "DWordWL"]
-cond = "μ"
 ref = "commit:c:address_incr"
 
 [[constraints.incr_decr]]
@@ -137,7 +136,6 @@ kind = "template"
 tag = "SUB"
 input = ["count", ["cast", 1, "DWordWL"]]
 output = ["cast", "count_decr", "DWordWL"]
-cond = "μ"
 ref = "commit:c:count_decr"
 
 [[constraints.incr_decr]]

From 4c86c39f9d0254217152f2daed8b0d305ec91aaf Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Thu, 12 Feb 2026 10:38:24 +0100
Subject: [PATCH 12/12] spec: COMMIT: list two possible optimizations

---
 spec/ecall.typ | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/spec/ecall.typ b/spec/ecall.typ
index 62539fa67..dd3544ef3 100644
--- a/spec/ecall.typ
+++ b/spec/ecall.typ
@@ -152,6 +152,15 @@ These are required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ`
 To pad this chip, use the below data.
 #render_chip_padding_table(chip, config)
 
-== Notes
+== 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.