From 0fd24b5cbeeee7e9245208efc3f5f0588cb5f455 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:41:32 +0200 Subject: [PATCH 1/4] spec: Draft FMA extension field accelerator --- spec/about_ecalls.typ | 4 +- spec/book.typ | 1 + spec/fext.typ | 75 +++++++++++++++++++++ spec/memory.typ | 1 + spec/src/fext_fma.toml | 141 ++++++++++++++++++++++++++++++++++++++++ spec/src/fext_load.toml | 66 +++++++++++++++++++ 6 files changed, 287 insertions(+), 1 deletion(-) create mode 100644 spec/fext.typ create mode 100644 spec/src/fext_fma.toml create mode 100644 spec/src/fext_load.toml diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index 9b37d5f21..d7954a703 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -31,4 +31,6 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / 64: `write` (@commit) / 93: `exit` (@halt) / -1: `SHA256` (@sha256) -/ -2: `KECCAK` (@keccak) \ No newline at end of file +/ -2: `KECCAK` (@keccak) +/-20: `FEXT_LOAD` (@fext) +/-21: `FEXT_FMA` (@fext) diff --git a/spec/book.typ b/spec/book.typ index 194689949..31867758a 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -51,6 +51,7 @@ ("commit.typ", [`COMMIT` chip], ), ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), + ("fext.typ", [Extension field accelerator], ), )), ("MATHEMATICS", ( ("limbs_and_carries.typ", [On limb decomposition and carries], ), diff --git a/spec/fext.typ b/spec/fext.typ new file mode 100644 index 000000000..f1f69ec43 --- /dev/null +++ b/spec/fext.typ @@ -0,0 +1,75 @@ +#import "/book.typ": book-page, aside +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + compute_nr_interactions, + render_constraint_table, + render_chip_assumptions, + render_chip_padding_table, +) + +#show: book-page("fext.typ") + +#let config = load_config() +#let loadchip = load_chip("src/fext_load.toml", config) +#let load = raw(loadchip.name) +#let fmachip = load_chip("src/fext_fma.toml", config) +#let fma = raw(fmachip.name) + +We introduce a set of chips for faster processing of numbers mod the native goldilocks prime, +or a degree three extension field thereof. +Our approach is to off an arithmetic black box, consisting of the *TODO* chips, +that operates on a separate memory domain, and the #load chip to bridge the gap +from normal byte-addressed RAM memory to this separate field-storage. +As noted in @memory, we reserve the domain separator values $3$, $4$ and $5$ for field-storage. + += The #load chip +#let nr_variables = total_nr_variables(loadchip) +#let nr_columns = total_nr_instantiated_columns(loadchip, config) +#let nr_interactions = compute_nr_interactions(loadchip) + +We use the #load chip to load the three composing coefficients from registers A1-A3 (in little-endian), +verify that all of them are in the correct range for a field element, +and then write them as field elements into field-storage. +We do this using #nr_variables variables spanning #nr_columns and #nr_interactions interactions. + +== Variables + +#render_chip_variable_table(loadchip, config) + +== Constraints + +#render_constraint_table(loadchip, config) + +== Padding + +#render_chip_padding_table(loadchip, config) + += The #fma chip +#let nr_variables = total_nr_variables(fmachip) +#let nr_columns = total_nr_instantiated_columns(fmachip, config) +#let nr_interactions = compute_nr_interactions(fmachip) + +To compute a fused multiply-add (FMA) operation `output = a * b + c`, we first load +everything from memory, passing the input (ABB) addresses in A0-A2 and the output address in A3. +Then we constrain the extension field operation, and write back to (ABB) memory. + +The extension field is expressed through three constant columns, $alpha$, $beta$ and $gamma$, +such that the defining polynomial is $X^3 - alpha X^2 - beta X - gamma = 0$, or alternatively, +$X^3 = alpha X^2 + beta X + gamma$. + +== Variables + +We express this chip using #nr_variables variables spanning #nr_columns and #nr_interactions interactions. + +#render_chip_variable_table(fmachip, config) + +== Constraints + +#render_constraint_table(fmachip, config) + +== Padding + +#render_chip_padding_table(fmachip, config) diff --git a/spec/memory.typ b/spec/memory.typ index bdd299b4b..610aa0e7d 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -30,6 +30,7 @@ For specific domains and domain separators, we use the following assignment. / RAM memory: $0$ / Registers: $1$ / Committed values: $2$ +/ (Extension) field values: $3$, $4$, $5$ On a high level, we ensure memory consistency by an interacting system of reads and writes to a lookup argument, combined with an initialization and finalization scheme. diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml new file mode 100644 index 000000000..d83c85172 --- /dev/null +++ b/spec/src/fext_fma.toml @@ -0,0 +1,141 @@ +name = "FEXT_FMA" + +[[variables.input]] +name = "input_addrs" +type = ["DWordWL", 3] +desc = "The addresses of `values`" +pad = 0 + +[[variables.input]] +name = "output_addr" +type = "DWordWL" +desc = "The address of `output`" +pad = 0 + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.auxiliary]] +name = "values" +type = [["BaseField", 3], 3] +desc = "The value to operate on: `a`, `b`, `c` in order to compute `a * b + c`" +pad = 0 + +[[variables.output]] +name = "output" +type = ["BaseField", 3] +desc = "The output value" +pad = 0 + +[[variables.constant]] +name = "α" +type = "BaseField" +desc = "The X^2 coefficient of the definining polynomial" + +[[variables.constant]] +name = "β" +type = "BaseField" +desc = "The X^1 coefficient of the definining polynomial" + +[[variables.constant]] +name = "γ" +type = "BaseField" +desc = "The X^0 coefficient of the definining polynomial" + +[[variables.virtual]] +name = "a" +type = ["BaseField", 3] +def = ["idx", "values", 0] +desc = "" + +[[variables.virtual]] +name = "b" +type = ["BaseField", 3] +def = ["idx", "values", 1] +desc = "" + +[[variables.virtual]] +name = "c" +type = ["BaseField", 3] +def = ["idx", "values", 2] +desc = "" + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, ["+", 10, "i"]], "DWordWL"], ["arr", ["idx", ["idx", "input_addrs", "i"], 0], ["idx", ["idx", "input_addrs", "i"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", ["idx", "input_addrs", "i"], 0], ["idx", ["idx", "input_addrs", "i"], 1], 0, 0, 0, 0, 0, 0] +iter = ["i", 0, 2] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 13], "DWordWL"], ["arr", ["idx", "output_addr", 0], ["idx", "output_addr", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", "output_addr", 0], ["idx", "output_addr", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "d"], ["idx", "input_addrs", "i"], ["arr", ["idx", ["idx", "values", "i"], "d"], 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0] +output = ["arr", ["idx", ["idx", "values", "i"], "d"], 0, 0, 0, 0, 0, 0, 0] +iters = [["d", 0, 2], ["i", 0, 2]] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "d"], "output_addr", ["arr", ["idx", "output", "d"], 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0] +multiplicity = "μ" +iter = ["d", 0, 2] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[0]` = a_0 b_0 + gamma (a_1 b_2 + a_2 b_1 + alpha a_2 b_2) + c_0$" +poly = ["-", ["idx", "output", 0], + ["*", ["idx", "a", 0], ["idx", "b", 0]], + ["*", "γ", ["+", + ["*", ["idx", "a", 1], ["idx", "b", 2]], + ["*", ["idx", "a", 2], ["idx", "b", 1]], + ["*", "α", ["idx", "a", 2], ["idx", "b", 2]]]], + ["idx", "c", 0]] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[1]` = a_0 b_1 + a_1 b_0 + beta (a_1 b_2 + a_2 b_1) + (alpha beta + gamma) a_2 b_2$" +poly = ["-", ["idx", "output", 1], + ["*", ["idx", "a", 0], ["idx", "b", 1]], + ["*", ["idx", "a", 1], ["idx", "b", 0]], + ["*", "β", ["idx", "a", 1], ["idx", "b", 2]], + ["*", "β", ["idx", "a", 2], ["idx", "b", 1]], + ["*", ["+", ["*", "α", "β"], "γ"], ["idx", "a", 2], ["idx", "b", 2]]] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[2]` = a_0 b_2 + a_1 b_1 + a_2 b_0 + alpha (a_1 b_2 + a_2 b_1) + (alpha^2 + beta) a_2 b_2$" +poly = ["-", ["idx", "output", 2], + ["*", ["idx", "a", 0], ["idx", "b", 2]], + ["*", ["idx", "a", 1], ["idx", "b", 1]], + ["*", ["idx", "a", 2], ["idx", "b", 0]], + ["*", "α", ["idx", "a", 1], ["idx", "b", 2]], + ["*", "α", ["idx", "a", 2], ["idx", "b", 1]], + ["*", ["+", ["*", "α", "α"], "β"], ["idx", "a", 2], ["idx", "b", 2]]] + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 21], ["-", ["^", 2, 32], 1]]] +multiplicity = ["-", "μ"] diff --git a/spec/src/fext_load.toml b/spec/src/fext_load.toml new file mode 100644 index 000000000..c8a88bfa3 --- /dev/null +++ b/spec/src/fext_load.toml @@ -0,0 +1,66 @@ +name = "FEXT_LOAD" + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.input]] +name = "addr" +type = "DWordWL" +desc = "The address at which to store the field element" +pad = 0 + +[[variables.input]] +name = "coeffs" +type = ["DWordWL", 3] +desc = "The extension field element coefficients, in native form" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", ["idx", "addr", 0], ["idx", "addr", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", "addr", 0], ["idx", "addr", 1], 0, 0, 0, 0, 0, 0] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [1, ["cast", ["*", 2, ["+", 11, "i"]], "DWordWL"], ["arr", ["idx", ["idx", "coeffs", "i"], 0], ["idx", ["idx", "coeffs", "i"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", ["idx", "coeffs", "i"], 0], ["idx", ["idx", "coeffs", "i"], 1], 0, 0, 0, 0, 0, 0] +multiplicity = "μ" +iter = ["i", 0, 2] + +[[constraints.all]] +kind = "interaction" +tag = "ALU" +input = [["idx", "coeffs", "i"], ["arr", 1, ["-", ["^", 2, 32], 1]], ["opsel", "LT"]] +output = ["cast", 1, "DWordWL"] +iter = ["i", 0, 2] +multiplicity = "μ" + +# This can either happen directly, or we introduce another dedicated MEMW accelerator? +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "i"], "addr", ["arr", ["+", ["*", ["^", 2, 32], ["idx", ["idx", "coeffs", "i"], 1]], ["idx", ["idx", "coeffs", "i"], 0]], 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0] +output = ["arr", ["+", ["*", ["^", 2, 32], ["idx", ["idx", "coeffs", "i"], 1]], ["idx", ["idx", "coeffs", "i"], 0]], 0, 0, 0, 0, 0, 0, 0] +iter = ["i", 0, 2] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 20], ["-", ["^", 2, 32], 1]]] +multiplicity = ["-", "μ"] From 87207dc358d5422194b7ca332d02cf5fbdfa710d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:44:33 +0200 Subject: [PATCH 2/4] Missing 'columns' --- spec/fext.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/fext.typ b/spec/fext.typ index f1f69ec43..3c875537c 100644 --- a/spec/fext.typ +++ b/spec/fext.typ @@ -33,7 +33,7 @@ As noted in @memory, we reserve the domain separator values $3$, $4$ and $5$ for We use the #load chip to load the three composing coefficients from registers A1-A3 (in little-endian), verify that all of them are in the correct range for a field element, and then write them as field elements into field-storage. -We do this using #nr_variables variables spanning #nr_columns and #nr_interactions interactions. +We do this using #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. == Variables @@ -62,7 +62,7 @@ $X^3 = alpha X^2 + beta X + gamma$. == Variables -We express this chip using #nr_variables variables spanning #nr_columns and #nr_interactions interactions. +We express this chip using #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. #render_chip_variable_table(fmachip, config) From 0b16c66b914a2584b516cd017043f98b4ed5e984 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:51:34 +0200 Subject: [PATCH 3/4] Add missing c terms --- spec/src/fext_fma.toml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index d83c85172..74838ce3a 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -121,7 +121,8 @@ poly = ["-", ["idx", "output", 1], ["*", ["idx", "a", 1], ["idx", "b", 0]], ["*", "β", ["idx", "a", 1], ["idx", "b", 2]], ["*", "β", ["idx", "a", 2], ["idx", "b", 1]], - ["*", ["+", ["*", "α", "β"], "γ"], ["idx", "a", 2], ["idx", "b", 2]]] + ["*", ["+", ["*", "α", "β"], "γ"], ["idx", "a", 2], ["idx", "b", 2]], + ["idx", "c", "1"]] [[constraints.all]] kind = "arith" @@ -132,7 +133,8 @@ poly = ["-", ["idx", "output", 2], ["*", ["idx", "a", 2], ["idx", "b", 0]], ["*", "α", ["idx", "a", 1], ["idx", "b", 2]], ["*", "α", ["idx", "a", 2], ["idx", "b", 1]], - ["*", ["+", ["*", "α", "α"], "β"], ["idx", "a", 2], ["idx", "b", 2]]] + ["*", ["+", ["*", "α", "α"], "β"], ["idx", "a", 2], ["idx", "b", 2]], + ["idx", "c", 2]] [[constraints.all]] kind = "interaction" From 97c5c69c614db79e472f38bbd30490d0c37f505b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 14:30:22 +0200 Subject: [PATCH 4/4] Fix string index --- spec/src/fext_fma.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index 74838ce3a..e50e83fd8 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -122,7 +122,7 @@ poly = ["-", ["idx", "output", 1], ["*", "β", ["idx", "a", 1], ["idx", "b", 2]], ["*", "β", ["idx", "a", 2], ["idx", "b", 1]], ["*", ["+", ["*", "α", "β"], "γ"], ["idx", "a", 2], ["idx", "b", 2]], - ["idx", "c", "1"]] + ["idx", "c", 1]] [[constraints.all]] kind = "arith"