From ffefc2165134600dcdf6e51a97ce70e2d2756e8a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 23 Jan 2026 16:58:18 +0100 Subject: [PATCH 1/6] spec: MUL: fix missing iters --- spec/src/mul.toml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/src/mul.toml b/spec/src/mul.toml index bf9ffc276..78dc070a5 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -63,8 +63,8 @@ name = "lhs_ext" 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_is_negative"]}, + {iter=[0, 3], poly=["idx", "lhs", "i"]}, + {iter=[4, 7], poly=["*", 0xFFFF, "lhs_is_negative"]}, ]} [[variables.virtual]] @@ -72,8 +72,8 @@ name = "rhs_ext" 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_is_negative"]}, + {iter=[0, 3], poly=["idx", "rhs", "i"]}, + {iter=[4, 7], poly=["*", 0xFFFF, "rhs_is_negative"]}, ]} [[variables.virtual]] @@ -81,8 +81,8 @@ name = "carry" type = ["B20", 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"]]]}, + {iter=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]]}, + {iter=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "res", "i"]]]}, ]} [[variables.virtual]] From 14e14735fb7b50e6542855314245ee396ffdf743 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 23 Jan 2026 16:59:07 +0100 Subject: [PATCH 2/6] spec: MUL: fix res slice in lookup contribution --- 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 78dc070a5..4a4dc93dd 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -166,7 +166,7 @@ name = "lookup" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "0"] -output = ["idx", "res", "0:4"] +output = ["idx", "res", "0:2"] multiplicity = ["-", "μ_lo"] ref = "mul:c:lookup_lo" @@ -174,6 +174,6 @@ ref = "mul:c:lookup_lo" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "1"] -output = ["idx", "res", "4:8"] +output = ["idx", "res", "2:4"] multiplicity = ["-", "μ_hi"] ref = "mul:c:lookup_hi" \ No newline at end of file From ad342e0df71c4daf3eb3c3ddeb1aa834f7e2edb9 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 26 Jan 2026 11:45:11 +0100 Subject: [PATCH 3/6] spec: MU: split `res` into `lo` and `hi` --- spec/mul.typ | 5 +++-- spec/src/mul.toml | 32 ++++++++++++++++++++++---------- 2 files changed, 25 insertions(+), 12 deletions(-) diff --git a/spec/mul.typ b/spec/mul.typ index 1892994f0..f1bc1c4ef 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -34,6 +34,7 @@ The following range checks are assumed to be performed/enforced outside of this #render_chip_assumptions(chip, config) == Constraints +For the purposes of the following discussion, we use `res: QuadWL` to refer to the concatenation of `lo` and `hi`. === Overview When `lhs` and `rhs` are _unsigned_ integers, computing their product $mod 2^128$ comes down to evaluating @@ -67,14 +68,14 @@ 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 definition. +This reduce-and-carry operation is constrained @mul:a:lo/@mul:a:hi 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) } $ with $#`carry`_(-1) = 0$ for simplicity. 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$. +With @mul:a:lo/@mul:a:hi 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. diff --git a/spec/src/mul.toml b/spec/src/mul.toml index 4a4dc93dd..fba9f9e8b 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -31,9 +31,15 @@ pad = 0 # Output [[variables.output]] -name = "res" -type = "QuadWL" -desc = "the (extended) multiplication result" +name = "lo" +type = "DWordWL" +desc = "the lower limbs of the (extended) multiplication result" +pad = 0 + +[[variables.output]] +name = "hi" +type = "DWordWL" +desc = "the upper limbs of the (extended) multiplication result" pad = 0 # Auxiliary @@ -81,8 +87,9 @@ name = "carry" type = ["B20", 4] desc = "carry values" def = {idx="i", polys=[ - {iter=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]]}, - {iter=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "res", "i"]]]}, + {iter=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "lo", 0]]]}, + {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "lo", 1]]]}, + {iter=[2, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "hi", ["-", "i", 2]]]]}, ]} [[variables.virtual]] @@ -116,9 +123,14 @@ desc = "`IS_HALF[rhs[i]]`" range = ["i", 0, 3] [[assumptions]] -desc = "`IS_WORD[res[i]]`" -range = ["i", 0, 3] -ref = "mul:a:res" +desc = "`IS_WORD[lo[i]]`" +iter = ["i", 0, 1] +ref = "mul:a:lo" + +[[assumptions]] +desc = "`IS_WORD[hi[i]]`" +iter = ["i", 0, 1] +ref = "mul:a:hi" # Constraints @@ -166,7 +178,7 @@ name = "lookup" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "0"] -output = ["idx", "res", "0:2"] +output = "lo" multiplicity = ["-", "μ_lo"] ref = "mul:c:lookup_lo" @@ -174,6 +186,6 @@ ref = "mul:c:lookup_lo" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "1"] -output = ["idx", "res", "2:4"] +output = "hi" multiplicity = ["-", "μ_hi"] ref = "mul:c:lookup_hi" \ No newline at end of file From 6e766cb797d9d2924695f0c85af8cb05ced66ee2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 26 Jan 2026 11:45:29 +0100 Subject: [PATCH 4/6] spec: MUL: replace `range` by `iter` --- 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 fba9f9e8b..e7de57cf0 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -116,11 +116,11 @@ pad = 0 [[assumptions]] desc = "`IS_HALF[lhs[i]]`" -range = ["i", 0, 3] +iter = ["i", 0, 3] [[assumptions]] desc = "`IS_HALF[rhs[i]]`" -range = ["i", 0, 3] +iter = ["i", 0, 3] [[assumptions]] desc = "`IS_WORD[lo[i]]`" @@ -156,7 +156,7 @@ ref = "mul:c:rhs_is_negative" kind = "interaction" tag = "IS_B20" input = [["idx", "carry", "i"]] -range = ["i", 0, 3] +iter = ["i", 0, 3] multiplicity = "μ_sum" ref = "mul:c:carry" @@ -168,7 +168,7 @@ name = "prod" kind = "arith" 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] +iter = ["i", 0, 3] ref = "mul:c:raw_product" [[constraint_groups]] From b97cf8694e1dc8283c7116a45ced4191e76b41e9 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 29 Jan 2026 11:26:54 +0100 Subject: [PATCH 5/6] spec: MUL: update `lo` and `hi` types + introduce `res` as virtual --- spec/mul.typ | 8 +++----- spec/src/mul.toml | 50 ++++++++++++++++++++++++++++++----------------- 2 files changed, 35 insertions(+), 23 deletions(-) diff --git a/spec/mul.typ b/spec/mul.typ index f1bc1c4ef..580424634 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -34,8 +34,6 @@ The following range checks are assumed to be performed/enforced outside of this #render_chip_assumptions(chip, config) == Constraints -For the purposes of the following discussion, we use `res: QuadWL` to refer to the concatenation of `lo` and `hi`. - === Overview When `lhs` and `rhs` are _unsigned_ integers, computing their product $mod 2^128$ comes down to evaluating $ @@ -68,14 +66,14 @@ 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:lo/@mul:a:hi and @mul:c:carry, combined with `carry`'s definition. +This reduce-and-carry operation is constrained by @mul:c:range_lo/@mul:c:range_hi 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) } $ with $#`carry`_(-1) = 0$ for simplicity. In other words: $#`res`_i equiv #`raw_product`_i + #`carry`_(i-1) (mod 2^32)$. -With @mul:a:lo/@mul:a:hi forcing $#`res`_i < 2^32$, $#`res`_i$ can only assume one value: $#`raw_product`_i + #`carry`_(i-1) mod 2^32$. +With @mul:c:range_lo/@mul:c:range_hi 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. @@ -84,7 +82,7 @@ In fact, in this situation it suffices to assert that $#`carry`_i < frac(p, 2^32 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. +We constrain `lhs_is_negative` and `rhs_is_negative` according to their definition; `lo`, `hi` and `carry` are appropriately range checked. #render_constraint_table(chip, config, groups: "def") === Product diff --git a/spec/src/mul.toml b/spec/src/mul.toml index e7de57cf0..e987b0f75 100644 --- a/spec/src/mul.toml +++ b/spec/src/mul.toml @@ -32,13 +32,13 @@ pad = 0 [[variables.output]] name = "lo" -type = "DWordWL" +type = "DWordHL" desc = "the lower limbs of the (extended) multiplication result" pad = 0 [[variables.output]] name = "hi" -type = "DWordWL" +type = "DWordHL" desc = "the upper limbs of the (extended) multiplication result" pad = 0 @@ -82,14 +82,23 @@ def = {idx="i", polys=[ {iter=[4, 7], poly=["*", 0xFFFF, "rhs_is_negative"]}, ]} +[[variables.virtual]] +name = "res" +type = "QuadWL" +desc = "concatenation of `lo` and `hi`." +def = {idx="i", polys=[ + {iter=[0, 1], poly=["idx", ["cast", "lo", "DWordWL"], "i"]}, + {iter=[2, 3], poly=["idx", ["cast", "hi", "DWordWL"], ["-", "i", 2]]}, +]} + + [[variables.virtual]] name = "carry" type = ["B20", 4] desc = "carry values" def = {idx="i", polys=[ - {iter=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "lo", 0]]]}, - {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", 1], ["idx", "carry", 0]], ["idx", "lo", 1]]]}, - {iter=[2, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "hi", ["-", "i", 2]]]]}, + {iter=0, poly=["*", ["^", 2, -32], ["-", ["idx", "raw_product", 0], ["idx", "res", 0]]]}, + {iter=[1, 3], poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "raw_product", "i"], ["idx", "carry", ["-", "i", 1]]], ["idx", "res", "i"]]]}, ]} [[variables.virtual]] @@ -122,17 +131,6 @@ iter = ["i", 0, 3] desc = "`IS_HALF[rhs[i]]`" iter = ["i", 0, 3] -[[assumptions]] -desc = "`IS_WORD[lo[i]]`" -iter = ["i", 0, 1] -ref = "mul:a:lo" - -[[assumptions]] -desc = "`IS_WORD[hi[i]]`" -iter = ["i", 0, 1] -ref = "mul:a:hi" - - # Constraints [[constraint_groups]] @@ -152,6 +150,22 @@ input = [["idx", "rhs", 3], "rhs_signed"] output = "rhs_is_negative" ref = "mul:c:rhs_is_negative" +[[constraints.def]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "lo", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ_sum" +ref = "mul:c:range_lo" + +[[constraints.def]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "hi", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ_sum" +ref = "mul:c:range_hi" + [[constraints.def]] kind = "interaction" tag = "IS_B20" @@ -178,7 +192,7 @@ name = "lookup" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "0"] -output = "lo" +output = ["cast", "lo", "DWordWL"] multiplicity = ["-", "μ_lo"] ref = "mul:c:lookup_lo" @@ -186,6 +200,6 @@ ref = "mul:c:lookup_lo" kind = "interaction" tag = "MUL" input = ["lhs", "lhs_signed", "rhs", "rhs_signed", "1"] -output = "hi" +output = ["cast", "hi", "DWordWL"] multiplicity = ["-", "μ_hi"] ref = "mul:c:lookup_hi" \ No newline at end of file From c7d56692a7d8e1afc3c92640d27696a4b967003c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 29 Jan 2026 11:36:08 +0100 Subject: [PATCH 6/6] spec: MUL: add note on future optimization --- spec/mul.typ | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/spec/mul.typ b/spec/mul.typ index 580424634..e9e7961d8 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -98,3 +98,12 @@ The #mul chip contributes the following to the lookup: The table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(chip, config) + +== Notes +- `lo` and `hi` are stored in `DWordHL`s (rather than `DWordWL`s) because of their values being range checked. + Since it is not required that both `μ_lo` and `μ_hi` are non-zero at the same time, one cannot safely assume their range to be checked elsewhere. + + As an optimization, one might be able to use a `DWordWL` and `DWordHL` to store `lo` and `hi`, + where one would decide which to store in which based on the multiplicities `μ_lo` and `μ_hi`; + the value sent into the lookup could then be assumed range-checked by the other side of the relation. + This optimization was not included at this moment because of its negative impact on the readability and verifiability of the chip. \ No newline at end of file