From 0223da9e459eb270fd544f4a496d4fce68063ab9 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 11:28:32 +0100
Subject: [PATCH 01/28] spec: support "sum" expression

---
 spec/expr.typ | 1 +
 1 file changed, 1 insertion(+)

diff --git a/spec/expr.typ b/spec/expr.typ
index df1ddb2e6..23c55e6b5 100644
--- a/spec/expr.typ
+++ b/spec/expr.typ
@@ -97,6 +97,7 @@
     "idx": (pp, rec, e) => $#rec(7, e.at(1))_(#rec(7, e.at(2)))$,
     "not": (pp, rec, e) => mwrap($1 - #rec(4, e.at(1))$, pp < 4),
     "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(5)).join($+$)$, pp < 5),
+    "sum": (pp, rec, e) => mwrap($sum_(#e.at(1).at(0)=#e.at(1).at(1))^#e.at(1).at(2) #e.slice(2).map(rec.with(5)).join($+$)$, pp < 5),
     "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(3)).join($dot$)$, pp < 3),
     "/": (pp, rec, e) => $#rec(3, e.at(1)) / #rec(3, e.at(2))$,
     "^": (pp, rec, e) => {

From f41d5f7c907c850d7455a653106417867b268774 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 11:28:52 +0100
Subject: [PATCH 02/28] spec: introduce "QuadHL" type

---
 spec/src/config.toml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/spec/src/config.toml b/spec/src/config.toml
index 1977b9155..ce62e0781 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -81,6 +81,14 @@ desc = """\
        The `Word` is the least significant digit.
        """
 
+[[variables.types]]
+label = "QuadHL"
+subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^128)$. \\
+       Represented as an array of eight `Half` variables.\
+       """
+
 # TODO: Having to define these manually will get tedious
 [[variables.types]]
 label = "Bit[3]"

From 14328e9a67ea408dcfdf656c40741c919f2835fe Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 11:29:06 +0100
Subject: [PATCH 03/28] spec: introduce MUL chip

---
 spec/book.typ     |   1 +
 spec/mul.typ      |  35 +++++++++
 spec/src/mul.toml | 177 ++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 213 insertions(+)
 create mode 100644 spec/mul.typ
 create mode 100644 spec/src/mul.toml

diff --git a/spec/book.typ b/spec/book.typ
index f50d7ed29..9866f03df 100644
--- a/spec/book.typ
+++ b/spec/book.typ
@@ -7,6 +7,7 @@
   title: "Lambda VM specification",
   summary: [
     #chapter("variables.typ")[Variables]
+    #chapter("mul.typ")[MUL chip]
   ]
 )
 
diff --git a/spec/mul.typ b/spec/mul.typ
new file mode 100644
index 000000000..47a23ac4d
--- /dev/null
+++ b/spec/mul.typ
@@ -0,0 +1,35 @@
+#import "/book.typ": book-page
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_column_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  render_constraint_table,
+  render_chip_assumptions,
+)
+
+#let config = load_config()
+#let chip = load_chip("src/mul.toml", config)
+
+#show: book-page.with(title: "MUL chip")
+
+
+#outline()
+
+= Columns
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+
+The `MUL` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+#render_chip_column_table(chip, config)
+
+
+= Assumptions
+#render_chip_assumptions(chip, config)
+
+
+= Constraints
+#render_constraint_table(chip, config, groups: "def")
+#render_constraint_table(chip, config, groups: "prod")
+*Note*: by the definition of `raw_product`, all components of the sum are of degree at most three.
+#render_constraint_table(chip, config, groups: "lookup")
\ No newline at end of file
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
new file mode 100644
index 000000000..1dc18997a
--- /dev/null
+++ b/spec/src/mul.toml
@@ -0,0 +1,177 @@
+name = "MUL"
+
+
+# Input
+
+[[variables.input]]
+name = "lhs"
+type = "DWordHL"
+desc = "the left hand operator."
+
+[[variables.input]]
+name = "lhs_signed"
+type = "Bit"
+desc = "whether to interpret `lhs` as a signed integer (1) or not (0)."
+
+[[variables.input]]
+name = "rhs"
+type = "DWordHL"
+desc = "the right hand operator."
+
+[[variables.input]]
+name = "rhs_signed"
+type = "Bit"
+desc = "whether to interpret `rhs` as a signed integer (1) or not (0)."
+
+
+# Output
+
+[[variables.output]]
+name = "res"
+type = "QuadHL"
+desc = "the (extended) multiplication result"
+
+# Auxiliary
+
+[[variables.auxiliary]]
+name = "lhs_msb"
+type = "Bit"
+desc = "the most significant bit of `lhs`"
+
+[[variables.auxiliary]]
+name = "rhs_msb"
+type = "Bit"
+desc = "the most significant bit of `rhs`"
+
+[[variables.auxiliary]]
+name = "raw_product"
+type = "Half[8]"
+desc = "raw multiplication output"
+
+# Virtual
+
+[[variables.virtual]]
+name = "lhs_ext"
+type = "Half[8]"
+desc = "sign-extended value of `lhs`"
+polys = [ 
+    ["idx", "lhs", 0],
+    ["idx", "lhs", 1],
+    ["idx", "lhs", 2],
+    ["idx", "lhs", 3],
+    ["*", 65535, "lhs_signed", "lhs_msb"],
+    ["*", 65535, "lhs_signed", "lhs_msb"],
+    ["*", 65535, "lhs_signed", "lhs_msb"],
+    ["*", 65535, "lhs_signed", "lhs_msb"],
+]
+
+[[variables.virtual]]
+name = "rhs_ext"
+type = "Half[8]"
+desc = "sign-extended value of `rhs`"
+polys = [ 
+    ["idx", "rhs", 0],
+    ["idx", "rhs", 1],
+    ["idx", "rhs", 2],
+    ["idx", "rhs", 3],
+    ["*", 65535, "rhs_signed", "rhs_msb"],
+    ["*", 65535, "rhs_signed", "rhs_msb"],
+    ["*", 65535, "rhs_signed", "rhs_msb"],
+    ["*", 65535, "rhs_signed", "rhs_msb"],
+]
+
+[[variables.virtual]]
+name = "carry"
+type = "Half[8]"
+desc = "carry values"
+polys = [
+    ["/", ["-", ["idx", "raw_product", 0], ["idx", "res", 0]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "res", 1]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 2], ["idx", "carry", 1]], ["idx", "res", 2]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 3], ["idx", "carry", 2]], ["idx", "res", 3]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 4], ["idx", "carry", 3]], ["idx", "res", 4]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 5], ["idx", "carry", 4]], ["idx", "res", 5]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 6], ["idx", "carry", 5]], ["idx", "res", 6]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 7], ["idx", "carry", 6]], ["idx", "res", 7]], 65535],
+]
+
+
+# Multiplicity
+
+[[variables.multiplicity]]
+name = "μ_lo"
+type = "BaseField"
+desc = ""
+
+[[variables.multiplicity]]
+name = "μ_hi"
+type = "BaseField"
+desc = ""
+
+# Assumptions
+
+[[assumptions]]
+desc = "IS_HALF[lhs[i]]"
+range = ["i", 0, 3]
+
+[[assumptions]]
+desc = "IS_HALF[rhs[i]]"
+range = ["i", 0, 3]
+
+
+# Constraints
+
+[[constraint_groups]]
+name = "def"
+
+[[constraints.def]]
+kind = "interaction"
+tag = "MSB16"
+input = [["idx", "lhs", 3]]
+output = "lhs_msb"
+multiplicity = ["+", "μ_lo", "μ_hi"]
+ref = "mul:c:lhs_msb"
+
+[[constraints.def]]
+kind = "interaction"
+tag = "MSB16"
+input = [["idx", "rhs", 3]]
+output = "rhs_msb"
+multiplicity = ["+", "μ_lo", "μ_hi"]
+ref = "mul:c:rhs_msb"
+
+[[constraints.def]]
+kind = "interaction"
+tag = "IS_HALF"
+input = [["idx", "carry", "i"]]
+range = ["i", 0, 7]
+multiplicity = ["+", "μ_lo", "μ_hi"]
+ref = "mul:c:carry"
+
+[[constraint_groups]]
+name = "prod"
+
+[[constraints.prod]]
+kind = "arith"
+constraint = "$#`raw_product[i]` = sum_(j=0)^i #`lhs_ext[i]` dot #`rhs_ext[i - j]`$"
+poly = ["-", ["idx", "raw_product", "i"], ["sum", ["j", 0, "i"], ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]]
+range = ["i", 0, 7]
+
+[[constraint_groups]]
+name = "lookup"
+
+[[constraints.lookup]]
+kind = "interaction"
+tag = "MUL"
+input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "0"]
+output = ["idx", "res", "0:4"]
+multiplicity = ["-", "μ_lo"]
+ref = "mul:c:lookup_lo"
+
+[[constraints.lookup]]
+kind = "interaction"
+tag = "MUL"
+input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "1"]
+output = ["idx", "res", "4:8"]
+multiplicity = ["-", "μ_hi"]
+ref = "mul:c:lookup_hi"
\ No newline at end of file

From ac020850efa5b37d355b11c9cc9ee7df5da12d6b Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 12:04:20 +0100
Subject: [PATCH 04/28] spec: Introduce QuadWL

---
 spec/src/config.toml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/spec/src/config.toml b/spec/src/config.toml
index ce62e0781..7c40d92ed 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -89,6 +89,14 @@ desc = """\
        Represented as an array of eight `Half` variables.\
        """
 
+[[variables.types]]
+label = "QuadWL"
+subtypes = ["Word", "Word", "Word", "Word"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^128)$. \\
+       Represented as an array of four `Word` variables.\
+       """
+
 # TODO: Having to define these manually will get tedious
 [[variables.types]]
 label = "Bit[3]"

From 025f409a6f8506739761eca0f5b8d7e3c486fc3d Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 12:04:30 +0100
Subject: [PATCH 05/28] spec: introduce B20[4]

---
 spec/src/config.toml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/spec/src/config.toml b/spec/src/config.toml
index 7c40d92ed..5d361c15c 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -27,6 +27,11 @@ label = "Half"
 subtypes = ["BaseField"]
 desc = "Variable that can only assume values in the range $[0, 2^16)$."
 
+[[variables.types]]
+label = "B20"
+subtypes = ["BaseField"]
+desc = "Variable that can only assume values in the range $[0, 2^20)$."
+
 [[variables.types]]
 label = "Word"
 subtypes = ["BaseField"]
@@ -123,6 +128,11 @@ label = "Half[8]"
 subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"]
 desc = "Eight halfwords"
 
+[[variables.types]]
+label = "B20[4]"
+subtypes = ["B20", "B20", "B20", "B20"]
+desc = "Four B20s"
+
 
 [variables.categories]
 all = ["input", "output", "auxiliary", "virtual", "multiplicity"]

From 214dc817241e42bb0a7dac8b96e28c6a8c037b18 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 12:05:12 +0100
Subject: [PATCH 06/28] spec: simplify MUL to 26 columns

---
 spec/src/mul.toml | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 1dc18997a..3ec427fb6 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -28,7 +28,7 @@ desc = "whether to interpret `rhs` as a signed integer (1) or not (0)."
 
 [[variables.output]]
 name = "res"
-type = "QuadHL"
+type = "QuadWL"
 desc = "the (extended) multiplication result"
 
 # Auxiliary
@@ -82,17 +82,13 @@ polys = [
 
 [[variables.virtual]]
 name = "carry"
-type = "Half[8]"
+type = "B20[4]"
 desc = "carry values"
 polys = [
-    ["/", ["-", ["idx", "raw_product", 0], ["idx", "res", 0]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "res", 1]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 2], ["idx", "carry", 1]], ["idx", "res", 2]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 3], ["idx", "carry", 2]], ["idx", "res", 3]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 4], ["idx", "carry", 3]], ["idx", "res", 4]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 5], ["idx", "carry", 4]], ["idx", "res", 5]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 6], ["idx", "carry", 5]], ["idx", "res", 6]], 65535],
-    ["/", ["-", ["+", ["idx", "raw_product", 7], ["idx", "carry", 6]], ["idx", "res", 7]], 65535],
+    ["/", ["-", ["+", ["idx", "raw_product", 0], ["*", 65536, ["idx",  "raw_product", 1]]], ["idx", "res", 0]], 4294967295],
+    ["/", ["-", ["+", ["idx", "raw_product", 2], ["*", 65536, ["idx",  "raw_product", 3]], ["idx", "carry", 0]], ["idx", "res", 1]], 4294967295],
+    ["/", ["-", ["+", ["idx", "raw_product", 4], ["*", 65536, ["idx",  "raw_product", 5]], ["idx", "carry", 1]], ["idx", "res", 2]], 4294967295],
+    ["/", ["-", ["+", ["idx", "raw_product", 6], ["*", 65536, ["idx",  "raw_product", 7]], ["idx", "carry", 2]], ["idx", "res", 3]], 4294967295],
 ]
 
 
@@ -142,7 +138,7 @@ ref = "mul:c:rhs_msb"
 
 [[constraints.def]]
 kind = "interaction"
-tag = "IS_HALF"
+tag = "IS_B20"
 input = [["idx", "carry", "i"]]
 range = ["i", 0, 7]
 multiplicity = ["+", "μ_lo", "μ_hi"]

From 793c4ad910858a5cdb52fb49baeab5938481a43b Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 14:37:09 +0100
Subject: [PATCH 07/28] spec: Fix expr-sum bug

---
 spec/expr.typ | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/expr.typ b/spec/expr.typ
index 23c55e6b5..62030622d 100644
--- a/spec/expr.typ
+++ b/spec/expr.typ
@@ -97,7 +97,7 @@
     "idx": (pp, rec, e) => $#rec(7, e.at(1))_(#rec(7, e.at(2)))$,
     "not": (pp, rec, e) => mwrap($1 - #rec(4, e.at(1))$, pp < 4),
     "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(5)).join($+$)$, pp < 5),
-    "sum": (pp, rec, e) => mwrap($sum_(#e.at(1).at(0)=#e.at(1).at(1))^#e.at(1).at(2) #e.slice(2).map(rec.with(5)).join($+$)$, pp < 5),
+    "sum": (pp, rec, e) => mwrap($sum_(#e.at(1).at(0)=#e.at(1).at(1))^#rec(10, e.at(1).at(2)) #e.slice(2).map(rec.with(5)).join($+$)$, pp < 5),
     "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(3)).join($dot$)$, pp < 3),
     "/": (pp, rec, e) => $#rec(3, e.at(1)) / #rec(3, e.at(2))$,
     "^": (pp, rec, e) => {

From 4375754f80eaf2d11258d9c7d8991063aae49f0e Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 14:37:39 +0100
Subject: [PATCH 08/28] spec: simplify MUL to 22 columns

---
 spec/src/config.toml | 20 ++++++++++++++++++++
 spec/src/mul.toml    | 38 ++++++++++++++++++++++----------------
 2 files changed, 42 insertions(+), 16 deletions(-)

diff --git a/spec/src/config.toml b/spec/src/config.toml
index 5d361c15c..bcefb2012 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -53,6 +53,16 @@ desc = """\
        Represented as an array of four `Byte` variables.\
        """
 
+[[variables.types]]
+label = "B35"
+subtypes = ["BaseField"]
+desc = "Variable that can only assume values in the range $[0, 2^35)$."
+
+[[variables.types]]
+label = "B51"
+subtypes = ["BaseField"]
+desc = "Variable that can only assume values in the range $[0, 2^51)$."
+
 [[variables.types]]
 label = "DWordBL"
 subtypes = ["Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte", "Byte"]
@@ -133,6 +143,16 @@ label = "B20[4]"
 subtypes = ["B20", "B20", "B20", "B20"]
 desc = "Four B20s"
 
+[[variables.types]]
+label = "B35[8]"
+subtypes = ["B35", "B35", "B35", "B35", "B35", "B35", "B35", "B35"]
+desc = "Eight B35s"
+
+[[variables.types]]
+label = "B51[4]"
+subtypes = ["B51", "B51", "B51", "B51"]
+desc = "Four B51s"
+
 
 [variables.categories]
 all = ["input", "output", "auxiliary", "virtual", "multiplicity"]
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 3ec427fb6..ea93dbd1b 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -45,7 +45,7 @@ desc = "the most significant bit of `rhs`"
 
 [[variables.auxiliary]]
 name = "raw_product"
-type = "Half[8]"
+type = "B51[4]"
 desc = "raw multiplication output"
 
 # Virtual
@@ -59,10 +59,10 @@ polys = [
     ["idx", "lhs", 1],
     ["idx", "lhs", 2],
     ["idx", "lhs", 3],
-    ["*", 65535, "lhs_signed", "lhs_msb"],
-    ["*", 65535, "lhs_signed", "lhs_msb"],
-    ["*", 65535, "lhs_signed", "lhs_msb"],
-    ["*", 65535, "lhs_signed", "lhs_msb"],
+    ["*", "0xFFFF", "lhs_signed", "lhs_msb"],
+    ["*", "0xFFFF", "lhs_signed", "lhs_msb"],
+    ["*", "0xFFFF", "lhs_signed", "lhs_msb"],
+    ["*", "0xFFFF", "lhs_signed", "lhs_msb"],
 ]
 
 [[variables.virtual]]
@@ -74,21 +74,27 @@ polys = [
     ["idx", "rhs", 1],
     ["idx", "rhs", 2],
     ["idx", "rhs", 3],
-    ["*", 65535, "rhs_signed", "rhs_msb"],
-    ["*", 65535, "rhs_signed", "rhs_msb"],
-    ["*", 65535, "rhs_signed", "rhs_msb"],
-    ["*", 65535, "rhs_signed", "rhs_msb"],
+    ["*", "0xFFFF", "rhs_signed", "rhs_msb"],
+    ["*", "0xFFFF", "rhs_signed", "rhs_msb"],
+    ["*", "0xFFFF", "rhs_signed", "rhs_msb"],
+    ["*", "0xFFFF", "rhs_signed", "rhs_msb"],
 ]
 
+[[variables.virtual]]
+name = "limb_product"
+type = "B35[8]"
+desc = "raw multiplication output"
+poly = ["sum", ["j", 0, "i"], ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]
+
 [[variables.virtual]]
 name = "carry"
 type = "B20[4]"
 desc = "carry values"
 polys = [
-    ["/", ["-", ["+", ["idx", "raw_product", 0], ["*", 65536, ["idx",  "raw_product", 1]]], ["idx", "res", 0]], 4294967295],
-    ["/", ["-", ["+", ["idx", "raw_product", 2], ["*", 65536, ["idx",  "raw_product", 3]], ["idx", "carry", 0]], ["idx", "res", 1]], 4294967295],
-    ["/", ["-", ["+", ["idx", "raw_product", 4], ["*", 65536, ["idx",  "raw_product", 5]], ["idx", "carry", 1]], ["idx", "res", 2]], 4294967295],
-    ["/", ["-", ["+", ["idx", "raw_product", 6], ["*", 65536, ["idx",  "raw_product", 7]], ["idx", "carry", 2]], ["idx", "res", 3]], 4294967295],
+    ["/", ["-", ["idx", "raw_product", 0], ["idx", "res", 0]], ["^", 2, 32]],
+    ["/", ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "res", 1]], ["^", 2, 32]],
+    ["/", ["-", ["+", ["idx", "raw_product", 2], ["idx", "carry", 1]], ["idx", "res", 2]], ["^", 2, 32]],
+    ["/", ["-", ["+", ["idx", "raw_product", 3], ["idx", "carry", 2]], ["idx", "res", 3]], ["^", 2, 32]],
 ]
 
 
@@ -149,9 +155,9 @@ name = "prod"
 
 [[constraints.prod]]
 kind = "arith"
-constraint = "$#`raw_product[i]` = sum_(j=0)^i #`lhs_ext[i]` dot #`rhs_ext[i - j]`$"
-poly = ["-", ["idx", "raw_product", "i"], ["sum", ["j", 0, "i"], ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]]
-range = ["i", 0, 7]
+constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^32 dot #`limb_product[2i + 1]`$"
+poly = ["-", ["+", ["idx", "limb_product", "2i"], ["*", ["^", 2, 32], ["idx", "limb_product", "2i+1"]]], ["idx", "raw_product", "i"]]
+range = ["i", 0, 3]
 
 [[constraint_groups]]
 name = "lookup"

From 2f8fe0bbe7be7dbe39bfd33d6f239136d65a745a Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 30 Dec 2025 14:39:19 +0100
Subject: [PATCH 09/28] spec: improve MUL readability

---
 spec/src/mul.toml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index ea93dbd1b..70a5403df 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -91,10 +91,10 @@ name = "carry"
 type = "B20[4]"
 desc = "carry values"
 polys = [
-    ["/", ["-", ["idx", "raw_product", 0], ["idx", "res", 0]], ["^", 2, 32]],
-    ["/", ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "res", 1]], ["^", 2, 32]],
-    ["/", ["-", ["+", ["idx", "raw_product", 2], ["idx", "carry", 1]], ["idx", "res", 2]], ["^", 2, 32]],
-    ["/", ["-", ["+", ["idx", "raw_product", 3], ["idx", "carry", 2]], ["idx", "res", 3]], ["^", 2, 32]],
+    ["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]],
+    ["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "res", 1]]],
+    ["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", 2], ["idx", "carry", 1]], ["idx", "res", 2]]],
+    ["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", 3], ["idx", "carry", 2]], ["idx", "res", 3]]],
 ]
 
 

From 7caf14f366fa3a0cf8651a5bfa34114090d0d3d3 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 09:24:45 +0100
Subject: [PATCH 10/28] spec: MUL: fix indexing

---
 spec/src/mul.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index b99d60898..a4e3720f1 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -142,7 +142,7 @@ name = "prod"
 [[constraints.prod]]
 kind = "arith"
 constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^32 dot #`limb_product[2i + 1]`$"
-poly = ["-", ["+", ["idx", "limb_product", "2i"], ["*", ["^", 2, 32], ["idx", "limb_product", "2i+1"]]], ["idx", "raw_product", "i"]]
+poly = ["-", ["+", ["idx", "limb_product", ["*", 2, "i"]], ["*", ["^", 2, 32], ["idx", "limb_product", ["+", ["*", 2, "i"], 1]]]], ["idx", "raw_product", "i"]]
 range = ["i", 0, 3]
 
 [[constraint_groups]]

From 971e3f5639393d315c5a2622777581e0cf2e66af Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 10:51:20 +0100
Subject: [PATCH 11/28] spec: MUL: refactor

---
 spec/mul.typ         |  1 -
 spec/src/config.toml |  5 ++++
 spec/src/mul.toml    | 61 ++++++++++++++++++++++++++++++++------------
 3 files changed, 50 insertions(+), 17 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index c3b0446b5..4d0e30c91 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -28,5 +28,4 @@ The `MUL` chip is comprised of #nr_variables variables that are expressed using
 = Constraints
 #render_constraint_table(chip, config, groups: "def")
 #render_constraint_table(chip, config, groups: "prod")
-*Note*: by the definition of `raw_product`, all components of the sum are of degree at most three.
 #render_constraint_table(chip, config, groups: "lookup")
\ No newline at end of file
diff --git a/spec/src/config.toml b/spec/src/config.toml
index 389e4b16a..e657ab23a 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -27,6 +27,11 @@ label = "Half"
 subtypes = ["BaseField"]
 desc = "Variable that can only assume values in the range $[0, 2^16)$."
 
+[[variables.types]]
+label = "B19"
+subtypes = ["BaseField"]
+desc = "Variable that can only assume values in the range $[0, 2^19)$."
+
 [[variables.types]]
 label = "B20"
 subtypes = ["BaseField"]
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index a4e3720f1..cb1d97ab2 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -34,14 +34,14 @@ desc = "the (extended) multiplication result"
 # Auxiliary
 
 [[variables.auxiliary]]
-name = "lhs_msb"
+name = "lhs_is_negative"
 type = "Bit"
-desc = "the most significant bit of `lhs`"
+desc = "whether `lhs` is negative (1) or not (0)"
 
 [[variables.auxiliary]]
-name = "rhs_msb"
+name = "rhs_is_negative"
 type = "Bit"
-desc = "the most significant bit of `rhs`"
+desc = "whether `rhs` is negative (1) or not (0)"
 
 [[variables.auxiliary]]
 name = "raw_product"
@@ -56,7 +56,7 @@ type = ["Half", 8]
 desc = "sign-extended value of `lhs`"
 def = {idx="i", polys=[
     {range=[0, 3], poly=["idx", "lhs", "i"]},
-    {range=[4, 7], poly=["*", 0xFFFF, "lhs_signed", "lhs_msb"]},
+    {range=[4, 7], poly=["*", 0xFFFF, "lhs_is_negative"]},
 ]}
 
 [[variables.virtual]]
@@ -65,24 +65,29 @@ type = ["Half", 8]
 desc = "sign-extended value of `rhs`"
 def = {idx="i", polys=[
     {range=[0, 3], poly=["idx", "rhs", "i"]},
-    {range=[4, 7], poly=["*", 0xFFFF, "rhs_signed", "rhs_msb"]},
+    {range=[4, 7], poly=["*", 0xFFFF, "rhs_is_negative"]},
 ]}
 
 [[variables.virtual]]
 name = "limb_product"
 type = ["B35", 8]
 desc = "raw multiplication output"
-def = ["sum", ["=", "j", 0], "i", ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]
+def = {idx="i", range=[0, 7], poly=["sum", ["=", "j", 0], "i", ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]}
 
 [[variables.virtual]]
 name = "carry"
-type = ["B20", 4]
+type = ["B19", 4]
 desc = "carry values"
 def = {idx="i", polys=[
     {range=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]]},
     {range=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "res", "i"]]]},
 ]}
 
+[[variables.virtual]]
+name = "μ_sum"
+type = "Bit"
+desc = "sum of multiplicies"
+def = ["+", "μ_lo", "μ_hi"]
 
 # Multiplicity
 
@@ -116,24 +121,48 @@ name = "def"
 kind = "interaction"
 tag = "MSB16"
 input = [["idx", "lhs", 3]]
-output = "lhs_msb"
-multiplicity = ["+", "μ_lo", "μ_hi"]
-ref = "mul:c:lhs_msb"
+output = "lhs_is_negative"
+multiplicity = "lhs_signed"
+ref = "mul:c:lhs_is_negative_if_signed"
+
+[[constraints.def]]
+kind = "arith"
+constraint = "$#`!lhs_signed` => #`lhs_is_negative` = 0$"
+poly = ["*", ["not", "lhs_signed"], "lhs_is_negative"]
+ref = "mul:c:lhs_is_negative_if_unsigned"
+
+[[constraints.def]]
+kind = "arith"
+constraint = "$#`lhs_signed` => #`μ_sum`$"
+poly = ["*", "lhs_signed", ["not", "μ_sum"]]
+ref = "mul:c:lhs_signed_implies_mu"
 
 [[constraints.def]]
 kind = "interaction"
 tag = "MSB16"
 input = [["idx", "rhs", 3]]
-output = "rhs_msb"
-multiplicity = ["+", "μ_lo", "μ_hi"]
-ref = "mul:c:rhs_msb"
+output = "rhs_is_negative"
+multiplicity = "rhs_signed"
+ref = "mul:c:rhs_is_negative"
+
+[[constraints.def]]
+kind = "arith"
+constraint = "$#`!rhs_signed` => #`rhs_is_negative` = 0$"
+poly = ["*", ["not", "rhs_signed"], "rhs_is_negative"]
+ref = "mul:c:rhs_is_negative_if_unsigned"
+
+[[constraints.def]]
+kind = "arith"
+constraint = "$#`rhs_signed` => #`μ_sum`$"
+poly = ["*", "rhs_signed", ["not", "μ_sum"]]
+ref = "mul:c:rhs_signed_implies_mu"
 
 [[constraints.def]]
 kind = "interaction"
-tag = "IS_B20"
+tag = "IS_B19"
 input = [["idx", "carry", "i"]]
 range = ["i", 0, 7]
-multiplicity = ["+", "μ_lo", "μ_hi"]
+multiplicity = "μ_sum"
 ref = "mul:c:carry"
 
 [[constraint_groups]]

From 3ab33e8d122a19f78be03ec8665e79dd59d3b166 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 12:19:12 +0100
Subject: [PATCH 12/28] spec: drop B20

---
 spec/src/config.toml | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/spec/src/config.toml b/spec/src/config.toml
index e657ab23a..bc92c39cf 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -32,11 +32,6 @@ label = "B19"
 subtypes = ["BaseField"]
 desc = "Variable that can only assume values in the range $[0, 2^19)$."
 
-[[variables.types]]
-label = "B20"
-subtypes = ["BaseField"]
-desc = "Variable that can only assume values in the range $[0, 2^20)$."
-
 [[variables.types]]
 label = "Word"
 subtypes = ["BaseField"]

From 7be71ee10a9c782cc8b8b7bd40b00d2e3535bad3 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 12:38:03 +0100
Subject: [PATCH 13/28] spec: MUL: fix raw_product relation

---
 spec/src/mul.toml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index cb1d97ab2..30e4a3776 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -170,8 +170,8 @@ name = "prod"
 
 [[constraints.prod]]
 kind = "arith"
-constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^32 dot #`limb_product[2i + 1]`$"
-poly = ["-", ["+", ["idx", "limb_product", ["*", 2, "i"]], ["*", ["^", 2, 32], ["idx", "limb_product", ["+", ["*", 2, "i"], 1]]]], ["idx", "raw_product", "i"]]
+constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^16 dot #`limb_product[2i + 1]`$"
+poly = ["-", ["+", ["idx", "limb_product", ["*", 2, "i"]], ["*", ["^", 2, 16], ["idx", "limb_product", ["+", ["*", 2, "i"], 1]]]], ["idx", "raw_product", "i"]]
 range = ["i", 0, 3]
 
 [[constraint_groups]]

From 8eb8f3b940ce20d7adb85bcb2781b5a10f622a77 Mon Sep 17 00:00:00 2001
From: Erik <159244975+erik-3milabs@users.noreply.github.com>
Date: Fri, 9 Jan 2026 13:39:55 +0100
Subject: [PATCH 14/28] spec: MUL: fix IS_B19 check range

Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech>
---
 spec/src/mul.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 30e4a3776..accb66175 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -161,7 +161,7 @@ ref = "mul:c:rhs_signed_implies_mu"
 kind = "interaction"
 tag = "IS_B19"
 input = [["idx", "carry", "i"]]
-range = ["i", 0, 7]
+range = ["i", 0, 3]
 multiplicity = "μ_sum"
 ref = "mul:c:carry"
 

From ab2d75279cdc27397958489d49367658935b0d4c Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 13:47:21 +0100
Subject: [PATCH 15/28] spec: MUL: add missing res range check assumption

---
 spec/src/mul.toml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index accb66175..58b29f094 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -111,6 +111,10 @@ range = ["i", 0, 3]
 desc = "`IS_HALF[rhs[i]]`"
 range = ["i", 0, 3]
 
+[[assumptions]]
+desc = "`IS_WORD[res[i]]`"
+range = ["i", 0, 3]
+
 
 # Constraints
 

From 44130918a19f30c6d0e8764e7a8e09ce32f3b4ac Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 9 Jan 2026 13:48:22 +0100
Subject: [PATCH 16/28] spec: MUL: remove superfluous/invalid constraints

---
 spec/src/mul.toml | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 58b29f094..a2b4f267f 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -135,12 +135,6 @@ constraint = "$#`!lhs_signed` => #`lhs_is_negative` = 0$"
 poly = ["*", ["not", "lhs_signed"], "lhs_is_negative"]
 ref = "mul:c:lhs_is_negative_if_unsigned"
 
-[[constraints.def]]
-kind = "arith"
-constraint = "$#`lhs_signed` => #`μ_sum`$"
-poly = ["*", "lhs_signed", ["not", "μ_sum"]]
-ref = "mul:c:lhs_signed_implies_mu"
-
 [[constraints.def]]
 kind = "interaction"
 tag = "MSB16"
@@ -155,12 +149,6 @@ constraint = "$#`!rhs_signed` => #`rhs_is_negative` = 0$"
 poly = ["*", ["not", "rhs_signed"], "rhs_is_negative"]
 ref = "mul:c:rhs_is_negative_if_unsigned"
 
-[[constraints.def]]
-kind = "arith"
-constraint = "$#`rhs_signed` => #`μ_sum`$"
-poly = ["*", "rhs_signed", ["not", "μ_sum"]]
-ref = "mul:c:rhs_signed_implies_mu"
-
 [[constraints.def]]
 kind = "interaction"
 tag = "IS_B19"

From 05d6b36fb60e57bf762d66896492a19d53f64367 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 12 Jan 2026 12:25:11 +0100
Subject: [PATCH 17/28] spec: MUL: leverage SIGN template

---
 spec/src/mul.toml | 29 ++++++++---------------------
 1 file changed, 8 insertions(+), 21 deletions(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index a2b4f267f..50bd7cabc 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -122,33 +122,19 @@ range = ["i", 0, 3]
 name = "def"
 
 [[constraints.def]]
-kind = "interaction"
-tag = "MSB16"
-input = [["idx", "lhs", 3]]
+kind = "template"
+tag = "SIGN"
+input = [["idx", "lhs", 3], "lhs_signed"]
 output = "lhs_is_negative"
-multiplicity = "lhs_signed"
-ref = "mul:c:lhs_is_negative_if_signed"
+ref = "mul:c:lhs_is_negative"
 
 [[constraints.def]]
-kind = "arith"
-constraint = "$#`!lhs_signed` => #`lhs_is_negative` = 0$"
-poly = ["*", ["not", "lhs_signed"], "lhs_is_negative"]
-ref = "mul:c:lhs_is_negative_if_unsigned"
-
-[[constraints.def]]
-kind = "interaction"
-tag = "MSB16"
-input = [["idx", "rhs", 3]]
+kind = "template"
+tag = "SIGN"
+input = [["idx", "rhs", 3], "rhs_signed"]
 output = "rhs_is_negative"
-multiplicity = "rhs_signed"
 ref = "mul:c:rhs_is_negative"
 
-[[constraints.def]]
-kind = "arith"
-constraint = "$#`!rhs_signed` => #`rhs_is_negative` = 0$"
-poly = ["*", ["not", "rhs_signed"], "rhs_is_negative"]
-ref = "mul:c:rhs_is_negative_if_unsigned"
-
 [[constraints.def]]
 kind = "interaction"
 tag = "IS_B19"
@@ -160,6 +146,7 @@ ref = "mul:c:carry"
 [[constraint_groups]]
 name = "prod"
 
+
 [[constraints.prod]]
 kind = "arith"
 constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^16 dot #`limb_product[2i + 1]`$"

From f42e7ca9ca939e0307a8ccd398bf648f2c34c1ad Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 12 Jan 2026 13:28:59 +0100
Subject: [PATCH 18/28] spec: MUL: fix index mistake

---
 spec/src/mul.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 50bd7cabc..e071cbb87 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -72,7 +72,7 @@ def = {idx="i", polys=[
 name = "limb_product"
 type = ["B35", 8]
 desc = "raw multiplication output"
-def = {idx="i", range=[0, 7], poly=["sum", ["=", "j", 0], "i", ["*", ["idx", "lhs_ext", "i"], ["idx", "rhs_ext", ["-", "i", "j"]]]]}
+def = {idx="i", range=[0, 7], poly=["sum", ["=", "j", 0], "i", ["*", ["idx", "lhs_ext", "j"], ["idx", "rhs_ext", ["-", "i", "j"]]]]}
 
 [[variables.virtual]]
 name = "carry"

From 46f74b1fdec19cb9f121848d235b582d3f7949ff Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 12 Jan 2026 16:47:31 +0100
Subject: [PATCH 19/28] spec: MUL: update description

---
 spec/mul.typ      | 60 ++++++++++++++++++++++++++++++++++++++++++++++-
 spec/src/mul.toml |  2 ++
 2 files changed, 61 insertions(+), 1 deletion(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index 4d0e30c91..b47bb1c0d 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -13,6 +13,8 @@
 
 #show: book-page.with(title: "MUL chip")
 
+#let mul = raw(chip.name)
+
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
@@ -20,12 +22,68 @@
 The `MUL` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_column_table(chip, config)
 
+#let stackrel(top, bottom) = {
+ $mat(delim: #none, top; bottom)$
+}
 
 = Assumptions
 #render_chip_assumptions(chip, config)
 
-
 = Constraints
+
+== Overview
+When `lhs` and `rhs` are _unsigned_ integers, computing their product $mod 2^128$ comes down to evaluating
+$
+(sum_(j=0)^3 2^(16j) dot #`lhs`_j) dot (sum_(i=0)^3 2^(16i) dot #`rhs`_i) mod 2^128.
+$
+If `lhs` and `rhs` are signed instead, the computation remains nearly identical: 
+one must sign extend `lhs` and `rhs` to twice their size --- forming `lhs_ext` and `rhs_ext` respectively --- and compute
+$
+(sum_(j=0)^7 2^(16j) dot #`lhs_ext`_j) dot (sum_(i=0)^7 2^(16i) dot #`rhs_ext`_i) mod 2^128.
+$
+where the limbs of `lhs_ext` and `rhs_ext` are treated as _unsigned_ integers.
+Note that by setting the extension limbs of `lhs` and/or `rhs` to $0$ when the integer is unsigned or signed and positive, the second formula still applies.
+Observe that we can rewrite this formula as
+$
+  &(sum_(j=0)^7 2^(16j) dot #`lhs_ext`_j) dot (sum_(i=0)^7 2^(16i) dot #`rhs_ext`_i) mod 2^128 \
+  &equiv sum_(j=0)^7 sum_(i=0)^7 2^(16(i+j)) dot #`lhs_ext`_j dot #`rhs_ext`_i mod 2^128 \
+  &stackrel(triangle, equiv) sum_(j=0)^7 sum_(i=0)^(7-j) 2^(16(i+j)) dot #`lhs_ext`_j dot #`rhs_ext`_i mod 2^128 \
+  &stackrel(square, equiv) sum_(j=0)^7 sum_(i=j)^(7) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
+  &stackrel(penta, equiv) sum_(i=0)^7 sum_(j=0)^(i) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
+  &equiv sum_(i=0)^7 2^(16i) dot sum_(j=0)^(i) #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
+$
+where at step
+- $triangle$ we can ignore $j > 7-i$, since that makes $2^(16(i+j)) equiv 0 mod 2^128$,
+- $square$ we rewrite the summation that $i$ iterates from $j$ to 7, rather than $0$ to $7-j$, and
+- $penta$ we swap the sums.
+Note that `limb_product` is defined as the second summation in this last formula.
+We can rewrite this as
+$
+  &sum_(i=0)^7 2^(16i) dot #`limb_product`_i mod 2^128 \
+  &equiv sum_(i=0)^3 sum_(k=0)^1 2^(16(2i+k)) dot #`limb_product`_(2i+k) mod 2^128 \
+  &equiv sum_(i=0)^3 2^(32i) dot sum_(k=0)^1 2^(16k) dot #`limb_product`_(2i+k) mod 2^128 \
+$
+where we now capture the second summation in the variable `raw_product` (see @mul:c:raw_product).
+
+At this point, the limbs in `raw_product` may require up to 51 bits to be represented.
+The last step is then to carry the overflow of each limb to the next, ensuring `res` represents the same value as `raw_product`, but with limbs in the range $[0, 2^32)$.
+This is simply constrained by `carry`'s definition and @mul:c:carry.
+From these two, we gather that
+$
+  #`raw_product`_0 - #`res`_0 in { i dot 2^32 | i in [0, 2^19) }
+$
+With @mul:a:res in place, $#`res`_0$ can only assume one value: the unique multiple of $2^32$ that is smaller than or equal to $#`raw_product`_0$.
+In other words, $#`res`_0$ is constrained to equal $#`raw_product`_0 mod 2^32$.
+The correctness of $#`res`_i$ for $i in [1, 3]$ follows analogously.
+
+== Definitions
+We constrain `lhs_is_negative` and `rhs_is_negative` according to their definition; `carry` is appropriately range checked.
 #render_constraint_table(chip, config, groups: "def")
+
+== Product
+@mul:c:raw_product defines `raw_product` in terms of the input values `lhs` and `rhs`.
 #render_constraint_table(chip, config, groups: "prod")
+
+== Lookup
+The #mul chip contributes the following to the lookup:
 #render_constraint_table(chip, config, groups: "lookup")
\ No newline at end of file
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index e071cbb87..6d0215860 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -114,6 +114,7 @@ range = ["i", 0, 3]
 [[assumptions]]
 desc = "`IS_WORD[res[i]]`"
 range = ["i", 0, 3]
+ref = "mul:a:res"
 
 
 # Constraints
@@ -152,6 +153,7 @@ kind = "arith"
 constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^16 dot #`limb_product[2i + 1]`$"
 poly = ["-", ["+", ["idx", "limb_product", ["*", 2, "i"]], ["*", ["^", 2, 16], ["idx", "limb_product", ["+", ["*", 2, "i"], 1]]]], ["idx", "raw_product", "i"]]
 range = ["i", 0, 3]
+ref = "mul:c:raw_product"
 
 [[constraint_groups]]
 name = "lookup"

From c6cb0ab6b94ea90ca61e926af3809693d91c3696 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 12 Jan 2026 16:59:57 +0100
Subject: [PATCH 20/28] spec: permit non-constant exponents

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

diff --git a/spec/expr.typ b/spec/expr.typ
index 547f2cad2..c452d70d3 100644
--- a/spec/expr.typ
+++ b/spec/expr.typ
@@ -145,8 +145,8 @@
     "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.mul)).join($dot$)$, pp < PREC.mul),
     "/": (pp, rec, e) => $#rec(PREC.div, e.at(1)) / #rec(PREC.div, e.at(2))$,
     "^": (pp, rec, e) => {
-      assert(type(e.at(1)) == int and type(e.at(2)) == int, message: "Can only exponentiate constants")
-      $#e.at(1)^#e.at(2)$
+      assert(type(e.at(1)) == int, message: "Can only exponentiate constants")
+      $#e.at(1)^#rec(PREC.MAX, e.at(2))$
     },
     "=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) = #rec(PREC.eq, e.at(2))$,
     ":=": (pp, rec, e) => $#rec(PREC.eq, e.at(1)) := #rec(PREC.eq, e.at(2))$,

From 3a20df6b19bb708d979742480c293a4276039002 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 12 Jan 2026 17:00:30 +0100
Subject: [PATCH 21/28] spec: MUL: drop `limb_product`

---
 spec/mul.typ      | 22 +++++++++-------------
 spec/src/mul.toml | 10 ++--------
 2 files changed, 11 insertions(+), 21 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index b47bb1c0d..0a9be4195 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -44,29 +44,25 @@ $
 where the limbs of `lhs_ext` and `rhs_ext` are treated as _unsigned_ integers.
 Note that by setting the extension limbs of `lhs` and/or `rhs` to $0$ when the integer is unsigned or signed and positive, the second formula still applies.
 Observe that we can rewrite this formula as
+#show math.equation: set block(breakable: true)
 $
   &(sum_(j=0)^7 2^(16j) dot #`lhs_ext`_j) dot (sum_(i=0)^7 2^(16i) dot #`rhs_ext`_i) mod 2^128 \
   &equiv sum_(j=0)^7 sum_(i=0)^7 2^(16(i+j)) dot #`lhs_ext`_j dot #`rhs_ext`_i mod 2^128 \
   &stackrel(triangle, equiv) sum_(j=0)^7 sum_(i=0)^(7-j) 2^(16(i+j)) dot #`lhs_ext`_j dot #`rhs_ext`_i mod 2^128 \
   &stackrel(square, equiv) sum_(j=0)^7 sum_(i=j)^(7) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
   &stackrel(penta, equiv) sum_(i=0)^7 sum_(j=0)^(i) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
-  &equiv sum_(i=0)^7 2^(16i) dot sum_(j=0)^(i) #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
+//   &equiv sum_(i=0)^7 2^(16i) dot sum_(j=0)^(i) #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
+  &equiv sum_(i=0)^3 sum_(k=0)^1 sum_(j=0)^(2i+k) 2^(16(2i+k)) dot #`lhs_ext`_j dot #`rhs_ext`_(2i+k-j) mod 2^128 \
+  &equiv sum_(i=0)^3 2^(32i) dot sum_(k=0)^1 2^(16k) dot sum_(j=0)^(2i+k) #`lhs_ext`_j dot #`rhs_ext`_(2i+k-j) mod 2^128
 $
 where at step
 - $triangle$ we can ignore $j > 7-i$, since that makes $2^(16(i+j)) equiv 0 mod 2^128$,
-- $square$ we rewrite the summation that $i$ iterates from $j$ to 7, rather than $0$ to $7-j$, and
+- $square$ we rewrite the second summation such that $i$ iterates from $j$ to 7, rather than $0$ to $7-j$, and
 - $penta$ we swap the sums.
-Note that `limb_product` is defined as the second summation in this last formula.
-We can rewrite this as
-$
-  &sum_(i=0)^7 2^(16i) dot #`limb_product`_i mod 2^128 \
-  &equiv sum_(i=0)^3 sum_(k=0)^1 2^(16(2i+k)) dot #`limb_product`_(2i+k) mod 2^128 \
-  &equiv sum_(i=0)^3 2^(32i) dot sum_(k=0)^1 2^(16k) dot #`limb_product`_(2i+k) mod 2^128 \
-$
-where we now capture the second summation in the variable `raw_product` (see @mul:c:raw_product).
 
-At this point, the limbs in `raw_product` may require up to 51 bits to be represented.
-The last step is then to carry the overflow of each limb to the next, ensuring `res` represents the same value as `raw_product`, but with limbs in the range $[0, 2^32)$.
+Note that `raw_product` captures the second summation in this last formula (see @mul:c:raw_product).
+However, the limbs in `raw_product` may require up to 51 bits to be represented.
+What remains then is to carry the overflow of each limb to the next, ensuring `res` represents the same value as `raw_product`, but with limbs in the range $[0, 2^32)$.
 This is simply constrained by `carry`'s definition and @mul:c:carry.
 From these two, we gather that
 $
@@ -81,7 +77,7 @@ We constrain `lhs_is_negative` and `rhs_is_negative` according to their definiti
 #render_constraint_table(chip, config, groups: "def")
 
 == Product
-@mul:c:raw_product defines `raw_product` in terms of the input values `lhs` and `rhs`.
+@mul:c:raw_product defines `raw_product` in terms of the (sign extended) input values `lhs` and `rhs`.
 #render_constraint_table(chip, config, groups: "prod")
 
 == Lookup
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 6d0215860..73a8a0b84 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -68,12 +68,6 @@ def = {idx="i", polys=[
     {range=[4, 7], poly=["*", 0xFFFF, "rhs_is_negative"]},
 ]}
 
-[[variables.virtual]]
-name = "limb_product"
-type = ["B35", 8]
-desc = "raw multiplication output"
-def = {idx="i", range=[0, 7], poly=["sum", ["=", "j", 0], "i", ["*", ["idx", "lhs_ext", "j"], ["idx", "rhs_ext", ["-", "i", "j"]]]]}
-
 [[variables.virtual]]
 name = "carry"
 type = ["B19", 4]
@@ -150,8 +144,8 @@ name = "prod"
 
 [[constraints.prod]]
 kind = "arith"
-constraint = "$#`raw_product[i]` = #`limb_product[2i]` + 2^16 dot #`limb_product[2i + 1]`$"
-poly = ["-", ["+", ["idx", "limb_product", ["*", 2, "i"]], ["*", ["^", 2, 16], ["idx", "limb_product", ["+", ["*", 2, "i"], 1]]]], ["idx", "raw_product", "i"]]
+constraint = "$#`raw_product[i]` = sum_(#`k`=0)^1 2^16 sum_(#`j`=0)^(2i+k) #`lhs_ext[j]` dot #`rhs_ext[2i+k-j]`$"
+poly = ["-", ["sum", ["=", "k", 0], "1", ["*", ["^", 2, ["*", 16, "k"]], ["sum", ["=", "j", 0], ["+", ["*", 2, "i"], "k"], ["*", ["idx", "lhs_ext", "j"], ["idx", "rhs_ext", ["-", ["+", ["*", 2, "i"], "k"], "j"]]]]]], ["idx", "raw_product", "i"]]
 range = ["i", 0, 3]
 ref = "mul:c:raw_product"
 

From 38e50861338fd4604e35e9e7b8dc2b8b0c95594b Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 11:26:36 +0100
Subject: [PATCH 22/28] spec: MUL: minor tweaks

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

diff --git a/spec/mul.typ b/spec/mul.typ
index 0a9be4195..ad1a82529 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -51,12 +51,11 @@ $
   &stackrel(triangle, equiv) sum_(j=0)^7 sum_(i=0)^(7-j) 2^(16(i+j)) dot #`lhs_ext`_j dot #`rhs_ext`_i mod 2^128 \
   &stackrel(square, equiv) sum_(j=0)^7 sum_(i=j)^(7) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
   &stackrel(penta, equiv) sum_(i=0)^7 sum_(j=0)^(i) 2^(16i) dot #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
-//   &equiv sum_(i=0)^7 2^(16i) dot sum_(j=0)^(i) #`lhs_ext`_j dot #`rhs_ext`_(i-j) mod 2^128 \
   &equiv sum_(i=0)^3 sum_(k=0)^1 sum_(j=0)^(2i+k) 2^(16(2i+k)) dot #`lhs_ext`_j dot #`rhs_ext`_(2i+k-j) mod 2^128 \
   &equiv sum_(i=0)^3 2^(32i) dot sum_(k=0)^1 2^(16k) dot sum_(j=0)^(2i+k) #`lhs_ext`_j dot #`rhs_ext`_(2i+k-j) mod 2^128
 $
 where at step
-- $triangle$ we can ignore $j > 7-i$, since that makes $2^(16(i+j)) equiv 0 mod 2^128$,
+- $triangle$ we can ignore $i > 7-j$, since that makes $2^(16(i+j)) equiv 0 mod 2^128$,
 - $square$ we rewrite the second summation such that $i$ iterates from $j$ to 7, rather than $0$ to $7-j$, and
 - $penta$ we swap the sums.
 
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 73a8a0b84..6dd7f5d12 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -144,7 +144,7 @@ name = "prod"
 
 [[constraints.prod]]
 kind = "arith"
-constraint = "$#`raw_product[i]` = sum_(#`k`=0)^1 2^16 sum_(#`j`=0)^(2i+k) #`lhs_ext[j]` dot #`rhs_ext[2i+k-j]`$"
+constraint = "$#`raw_product[i]` = sum_(#`k`=0)^1 2^(16k) sum_(#`j`=0)^(2i+k) #`lhs_ext[j]` dot #`rhs_ext[2i+k-j]`$"
 poly = ["-", ["sum", ["=", "k", 0], "1", ["*", ["^", 2, ["*", 16, "k"]], ["sum", ["=", "j", 0], ["+", ["*", 2, "i"], "k"], ["*", ["idx", "lhs_ext", "j"], ["idx", "rhs_ext", ["-", ["+", ["*", 2, "i"], "k"], "j"]]]]]], ["idx", "raw_product", "i"]]
 range = ["i", 0, 3]
 ref = "mul:c:raw_product"

From 272006b770dcf0ca2bcb3475861e08e26a1ddc71 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 11:28:30 +0100
Subject: [PATCH 23/28] spec: MUL: bump headers

---
 spec/mul.typ | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index ad1a82529..559bd44c9 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -15,7 +15,9 @@
 
 #let mul = raw(chip.name)
 
-= Columns
+= #mul chip
+
+== Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
 
@@ -26,12 +28,12 @@ The `MUL` chip is comprised of #nr_variables variables that are expressed using
  $mat(delim: #none, top; bottom)$
 }
 
-= Assumptions
+== Assumptions
 #render_chip_assumptions(chip, config)
 
-= Constraints
+== Constraints
 
-== Overview
+=== Overview
 When `lhs` and `rhs` are _unsigned_ integers, computing their product $mod 2^128$ comes down to evaluating
 $
 (sum_(j=0)^3 2^(16j) dot #`lhs`_j) dot (sum_(i=0)^3 2^(16i) dot #`rhs`_i) mod 2^128.
@@ -71,14 +73,14 @@ With @mul:a:res in place, $#`res`_0$ can only assume one value: the unique multi
 In other words, $#`res`_0$ is constrained to equal $#`raw_product`_0 mod 2^32$.
 The correctness of $#`res`_i$ for $i in [1, 3]$ follows analogously.
 
-== Definitions
+=== Definitions
 We constrain `lhs_is_negative` and `rhs_is_negative` according to their definition; `carry` is appropriately range checked.
 #render_constraint_table(chip, config, groups: "def")
 
-== Product
+=== Product
 @mul:c:raw_product defines `raw_product` in terms of the (sign extended) input values `lhs` and `rhs`.
 #render_constraint_table(chip, config, groups: "prod")
 
-== Lookup
+=== Lookup
 The #mul chip contributes the following to the lookup:
 #render_constraint_table(chip, config, groups: "lookup")
\ No newline at end of file

From f6797b94df95613141078495710190b878feb32d Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 11:35:14 +0100
Subject: [PATCH 24/28] spec: MUL: update description

---
 spec/mul.typ | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index 559bd44c9..7cf3fb54c 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -29,6 +29,7 @@ The `MUL` chip is comprised of #nr_variables variables that are expressed using
 }
 
 == Assumptions
+The following range checks are assumed to be performed/enforced outside of this chip:
 #render_chip_assumptions(chip, config)
 
 == Constraints
@@ -39,13 +40,13 @@ $
 (sum_(j=0)^3 2^(16j) dot #`lhs`_j) dot (sum_(i=0)^3 2^(16i) dot #`rhs`_i) mod 2^128.
 $
 If `lhs` and `rhs` are signed instead, the computation remains nearly identical: 
-one must sign extend `lhs` and `rhs` to twice their size --- forming `lhs_ext` and `rhs_ext` respectively --- and compute
+based on their signs, one must either zero or one-extend `lhs` and `rhs` --- forming `lhs_ext` and `rhs_ext` respectively --- and compute their product $mod 2^128$:
 $
 (sum_(j=0)^7 2^(16j) dot #`lhs_ext`_j) dot (sum_(i=0)^7 2^(16i) dot #`rhs_ext`_i) mod 2^128.
 $
-where the limbs of `lhs_ext` and `rhs_ext` are treated as _unsigned_ integers.
-Note that by setting the extension limbs of `lhs` and/or `rhs` to $0$ when the integer is unsigned or signed and positive, the second formula still applies.
-Observe that we can rewrite this formula as
+where `lhs_ext` and `rhs_ext` are treated as _unsigned_ integers.
+Note that by setting the extension limbs of `lhs` and/or `rhs` to $0$ when the integer is (i) unsigned or (ii) signed and non-negative, this second formula still applies.
+For the purposes of constraining the multiplication operation, we rewrite this formula as
 #show math.equation: set block(breakable: true)
 $
   &(sum_(j=0)^7 2^(16j) dot #`lhs_ext`_j) dot (sum_(i=0)^7 2^(16i) dot #`rhs_ext`_i) mod 2^128 \

From dbe8dc0e3e7092872e7cb0cc7a6d9b58c530c79a Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 13:03:54 +0100
Subject: [PATCH 25/28] spec: MUL: update to IS_B20

---
 spec/mul.typ         | 25 ++++++++++++++++---------
 spec/src/config.toml |  4 ++--
 spec/src/mul.toml    |  4 ++--
 3 files changed, 20 insertions(+), 13 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index 7cf3fb54c..247392220 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -62,17 +62,24 @@ where at step
 - $square$ we rewrite the second summation such that $i$ iterates from $j$ to 7, rather than $0$ to $7-j$, and
 - $penta$ we swap the sums.
 
-Note that `raw_product` captures the second summation in this last formula (see @mul:c:raw_product).
-However, the limbs in `raw_product` may require up to 51 bits to be represented.
-What remains then is to carry the overflow of each limb to the next, ensuring `res` represents the same value as `raw_product`, but with limbs in the range $[0, 2^32)$.
-This is simply constrained by `carry`'s definition and @mul:c:carry.
-From these two, we gather that
+We let `raw_product` capture the second summation in this last formula (see @mul:c:raw_product).
+By construction, $#`raw_product`_i < 2^51$ for all $i in [0, 3]$, far exceeding the 32-bits that fit in a single `Word`-limb.
+What remains then is to reduce each limb of `raw_product` $mod 2^32$, carrying the overflow of each limb to the next, constructing the output `res` in doing so.
+
+This reduce-and-carry operation is constrained @mul:a:res and @mul:c:carry, combined with `carry`'s eloquent definition.
+@mul:c:carry and `carry`'s definition enforce that
 $
-  #`raw_product`_0 - #`res`_0 in { i dot 2^32 | i in [0, 2^19) }
+  forall i in [0, 3]: #`raw_product`_i + #`carry`_(i-1) - #`res`_i in { k dot 2^32 | k in [0, 2^20) }
 $
-With @mul:a:res in place, $#`res`_0$ can only assume one value: the unique multiple of $2^32$ that is smaller than or equal to $#`raw_product`_0$.
-In other words, $#`res`_0$ is constrained to equal $#`raw_product`_0 mod 2^32$.
-The correctness of $#`res`_i$ for $i in [1, 3]$ follows analogously.
+with $#`carry`_(-1) = 0$ for simplicity.
+In other words: $#`res`_i >= #`raw_product`_i + #`carry`_(i-1) mod 2^32$.
+With @mul:a:res forcing $#`res`_i < 2^32$, $#`res`_i$ can only assume one value: $#`raw_product`_i + #`carry`_(i-1) mod 2^32$.
+
+*Note*: one may have observed that @mul:c:carry requires $#`carry`_i in [0, 2^20)$, while no limb of a valid carry value would ever exceed $2^19$.
+This is indeed the case.
+However, there is some slack in how tight one has to constrain the `carry` values.
+In fact, in this situation it suffices to assert that $#`carry`_i < frac(p, 2^32, style: "skewed") approx 2^31$, where $p$ denotes the field's modulus.
+Given that other chips also use 20-bit lookups, using `IS_B20` makes for a simpler design.
 
 === Definitions
 We constrain `lhs_is_negative` and `rhs_is_negative` according to their definition; `carry` is appropriately range checked.
diff --git a/spec/src/config.toml b/spec/src/config.toml
index bc92c39cf..389e4b16a 100644
--- a/spec/src/config.toml
+++ b/spec/src/config.toml
@@ -28,9 +28,9 @@ subtypes = ["BaseField"]
 desc = "Variable that can only assume values in the range $[0, 2^16)$."
 
 [[variables.types]]
-label = "B19"
+label = "B20"
 subtypes = ["BaseField"]
-desc = "Variable that can only assume values in the range $[0, 2^19)$."
+desc = "Variable that can only assume values in the range $[0, 2^20)$."
 
 [[variables.types]]
 label = "Word"
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index 6dd7f5d12..d952f7bed 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -70,7 +70,7 @@ def = {idx="i", polys=[
 
 [[variables.virtual]]
 name = "carry"
-type = ["B19", 4]
+type = ["B20", 4]
 desc = "carry values"
 def = {idx="i", polys=[
     {range=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]]},
@@ -132,7 +132,7 @@ ref = "mul:c:rhs_is_negative"
 
 [[constraints.def]]
 kind = "interaction"
-tag = "IS_B19"
+tag = "IS_B20"
 input = [["idx", "carry", "i"]]
 range = ["i", 0, 3]
 multiplicity = "μ_sum"

From 54eb6732b7ac09f11e024e81628dfa54d6d71c2f Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 13:42:19 +0100
Subject: [PATCH 26/28] spec: MUL: remove 'eloquent'

---
 spec/mul.typ | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index 247392220..a51dab2e8 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -66,7 +66,7 @@ We let `raw_product` capture the second summation in this last formula (see @mul
 By construction, $#`raw_product`_i < 2^51$ for all $i in [0, 3]$, far exceeding the 32-bits that fit in a single `Word`-limb.
 What remains then is to reduce each limb of `raw_product` $mod 2^32$, carrying the overflow of each limb to the next, constructing the output `res` in doing so.
 
-This reduce-and-carry operation is constrained @mul:a:res and @mul:c:carry, combined with `carry`'s eloquent definition.
+This reduce-and-carry operation is constrained @mul:a:res and @mul:c:carry, combined with `carry`'s definition.
 @mul:c:carry and `carry`'s definition enforce that
 $
   forall i in [0, 3]: #`raw_product`_i + #`carry`_(i-1) - #`res`_i in { k dot 2^32 | k in [0, 2^20) }

From 0b7fc8a9eb28c88ca440fbea3c6a86e41c647b05 Mon Sep 17 00:00:00 2001
From: Erik <159244975+erik-3milabs@users.noreply.github.com>
Date: Tue, 13 Jan 2026 15:06:31 +0100
Subject: [PATCH 27/28] Apply suggestions from code review

Thanks Robin!

Co-authored-by: Robin Jadoul <robin.jadoul@3milabs.tech>
---
 spec/mul.typ      | 2 +-
 spec/src/mul.toml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/mul.typ b/spec/mul.typ
index a51dab2e8..92fafe26b 100644
--- a/spec/mul.typ
+++ b/spec/mul.typ
@@ -72,7 +72,7 @@ $
   forall i in [0, 3]: #`raw_product`_i + #`carry`_(i-1) - #`res`_i in { k dot 2^32 | k in [0, 2^20) }
 $
 with $#`carry`_(-1) = 0$ for simplicity.
-In other words: $#`res`_i >= #`raw_product`_i + #`carry`_(i-1) mod 2^32$.
+In other words: $#`res`_i equiv #`raw_product`_i + #`carry`_(i-1) (mod 2^32)$.
 With @mul:a:res forcing $#`res`_i < 2^32$, $#`res`_i$ can only assume one value: $#`raw_product`_i + #`carry`_(i-1) mod 2^32$.
 
 *Note*: one may have observed that @mul:c:carry requires $#`carry`_i in [0, 2^20)$, while no limb of a valid carry value would ever exceed $2^19$.
diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index d952f7bed..c37cec181 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -79,7 +79,7 @@ def = {idx="i", polys=[
 
 [[variables.virtual]]
 name = "μ_sum"
-type = "Bit"
+type = "BaseField"
 desc = "sum of multiplicies"
 def = ["+", "μ_lo", "μ_hi"]
 

From 215f0e500cef6f828d3d3fc05c24d47101f2b8bb Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 13 Jan 2026 15:07:59 +0100
Subject: [PATCH 28/28] spec: MUL: define padding

---
 spec/src/mul.toml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/spec/src/mul.toml b/spec/src/mul.toml
index c37cec181..bf9ffc276 100644
--- a/spec/src/mul.toml
+++ b/spec/src/mul.toml
@@ -7,21 +7,25 @@ name = "MUL"
 name = "lhs"
 type = "DWordHL"
 desc = "the left hand operator."
+pad = 0
 
 [[variables.input]]
 name = "lhs_signed"
 type = "Bit"
 desc = "whether to interpret `lhs` as a signed integer (1) or not (0)."
+pad = 0
 
 [[variables.input]]
 name = "rhs"
 type = "DWordHL"
 desc = "the right hand operator."
+pad = 0
 
 [[variables.input]]
 name = "rhs_signed"
 type = "Bit"
 desc = "whether to interpret `rhs` as a signed integer (1) or not (0)."
+pad = 0
 
 
 # Output
@@ -30,6 +34,7 @@ desc = "whether to interpret `rhs` as a signed integer (1) or not (0)."
 name = "res"
 type = "QuadWL"
 desc = "the (extended) multiplication result"
+pad = 0
 
 # Auxiliary
 
@@ -37,16 +42,19 @@ desc = "the (extended) multiplication result"
 name = "lhs_is_negative"
 type = "Bit"
 desc = "whether `lhs` is negative (1) or not (0)"
+pad = 0
 
 [[variables.auxiliary]]
 name = "rhs_is_negative"
 type = "Bit"
 desc = "whether `rhs` is negative (1) or not (0)"
+pad = 0
 
 [[variables.auxiliary]]
 name = "raw_product"
 type = ["B51", 4]
 desc = "raw multiplication output"
+pad = 0
 
 # Virtual
 
@@ -89,11 +97,13 @@ def = ["+", "μ_lo", "μ_hi"]
 name = "μ_lo"
 type = "BaseField"
 desc = ""
+pad = 0
 
 [[variables.multiplicity]]
 name = "μ_hi"
 type = "BaseField"
 desc = ""
+pad = 0
 
 # Assumptions