From ba20900a612ccb235e7bdfd88cbb626ec58e8694 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:41:32 +0200 Subject: [PATCH 01/10] spec: Draft FMA extension field accelerator --- spec/about_ecalls.typ | 2 + 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, 286 insertions(+) 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 1c1f32095..b5667ed1e 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -34,3 +34,5 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / -2: `KECCAK` (@keccak) / -11: `ECSM`/`secp256k1` (@ecsm) / -12: `ECSM`/`secp256r1` (@ecsm) +/-20: `FEXT_LOAD` (@fext) +/-21: `FEXT_FMA` (@fext) diff --git a/spec/book.typ b/spec/book.typ index e8eb1855c..052f134bd 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -53,6 +53,7 @@ ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), ("ecsm.typ", [`ECSM` 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 62fb29b5f3748193dd93bd2cc4c27d972d43f78d Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:44:33 +0200 Subject: [PATCH 02/10] 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 c94767ab951a389aa45895f8ac8ca06b6763a21e Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 13:51:34 +0200 Subject: [PATCH 03/10] 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 a63f3c0ed74f4dea47ded5804207b64923233df5 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 14 Jul 2026 14:30:22 +0200 Subject: [PATCH 04/10] 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" From 9f43a999bbb96498d17866a4988996081437ecd6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 20 Jul 2026 15:45:17 +0200 Subject: [PATCH 05/10] Chip codes Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/fext_fma.toml | 1 + spec/src/fext_load.toml | 1 + 2 files changed, 2 insertions(+) diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index e50e83fd8..15c8123a3 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -1,4 +1,5 @@ name = "FEXT_FMA" +code = "FMA" [[variables.input]] name = "input_addrs" diff --git a/spec/src/fext_load.toml b/spec/src/fext_load.toml index c8a88bfa3..80c247972 100644 --- a/spec/src/fext_load.toml +++ b/spec/src/fext_load.toml @@ -1,4 +1,5 @@ name = "FEXT_LOAD" +code = "FXL" [[variables.input]] name = "timestamp" From 34d5ab9703af5a8be2286277828bc3b1063b17aa Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 20 Jul 2026 15:46:28 +0200 Subject: [PATCH 06/10] Rendering and typos Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/about_ecalls.typ | 4 ++-- spec/fext.typ | 2 +- spec/src/fext_fma.toml | 12 ++++++------ 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index b5667ed1e..a6f739a28 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -34,5 +34,5 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / -2: `KECCAK` (@keccak) / -11: `ECSM`/`secp256k1` (@ecsm) / -12: `ECSM`/`secp256r1` (@ecsm) -/-20: `FEXT_LOAD` (@fext) -/-21: `FEXT_FMA` (@fext) +/ -20: `FEXT_LOAD` (@fext) +/ -21: `FEXT_FMA` (@fext) diff --git a/spec/fext.typ b/spec/fext.typ index 3c875537c..728a8be8b 100644 --- a/spec/fext.typ +++ b/spec/fext.typ @@ -20,7 +20,7 @@ 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, +Our approach is to offer 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. diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index 15c8123a3..962ca20e2 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -34,17 +34,17 @@ pad = 0 [[variables.constant]] name = "α" type = "BaseField" -desc = "The X^2 coefficient of the definining polynomial" +desc = "The $#`X`^2$ coefficient of the definining polynomial" [[variables.constant]] name = "β" type = "BaseField" -desc = "The X^1 coefficient of the definining polynomial" +desc = "The $#`X`^1$ coefficient of the definining polynomial" [[variables.constant]] name = "γ" type = "BaseField" -desc = "The X^0 coefficient of the definining polynomial" +desc = "The $#`X`^0$ coefficient of the definining polynomial" [[variables.virtual]] name = "a" @@ -105,7 +105,7 @@ 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$" +constraint = "$#`output[0]` = a_0 b_0 + gamma (a_1 b_2 + a_2 b_1 + alpha dot a_2 b_2) + c_0$" poly = ["-", ["idx", "output", 0], ["*", ["idx", "a", 0], ["idx", "b", 0]], ["*", "γ", ["+", @@ -116,7 +116,7 @@ poly = ["-", ["idx", "output", 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$" +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 + c_1$" poly = ["-", ["idx", "output", 1], ["*", ["idx", "a", 0], ["idx", "b", 1]], ["*", ["idx", "a", 1], ["idx", "b", 0]], @@ -127,7 +127,7 @@ poly = ["-", ["idx", "output", 1], [[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$" +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 + c_2$" poly = ["-", ["idx", "output", 2], ["*", ["idx", "a", 0], ["idx", "b", 2]], ["*", ["idx", "a", 1], ["idx", "b", 1]], From 66b3b9d16dcdbc000b8e43b29e36cd8d9c893a57 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 20 Jul 2026 15:48:31 +0200 Subject: [PATCH 07/10] timestamp separation --- spec/src/fext_fma.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index 962ca20e2..8d4dc04c3 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -91,7 +91,7 @@ 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] +input = [["+", 3, "d"], ["idx", "input_addrs", "i"], ["arr", ["idx", ["idx", "values", "i"], "d"], 0, 0, 0, 0, 0, 0, 0], ["+", "timestamp", "i"], 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 = "μ" @@ -99,7 +99,7 @@ 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] +input = [["+", 3, "d"], "output_addr", ["arr", ["idx", "output", "d"], 0, 0, 0, 0, 0, 0, 0], ["+", "timestamp", 3], 0, 0, 0] multiplicity = "μ" iter = ["d", 0, 2] From 911263ebe291803b993d3ca29b1c993a1008d5c9 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 20 Jul 2026 16:57:31 +0200 Subject: [PATCH 08/10] FEXT_ZERO --- spec/about_ecalls.typ | 1 + spec/fext.typ | 21 +++++++++++++++++++- spec/src/fext_zero.toml | 44 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 65 insertions(+), 1 deletion(-) create mode 100644 spec/src/fext_zero.toml diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index a6f739a28..f4ae00a23 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -36,3 +36,4 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / -12: `ECSM`/`secp256r1` (@ecsm) / -20: `FEXT_LOAD` (@fext) / -21: `FEXT_FMA` (@fext) +/ -22: `FEXT_ZERO` (@fext) diff --git a/spec/fext.typ b/spec/fext.typ index 728a8be8b..d6ba762dd 100644 --- a/spec/fext.typ +++ b/spec/fext.typ @@ -17,10 +17,12 @@ #let load = raw(loadchip.name) #let fmachip = load_chip("src/fext_fma.toml", config) #let fma = raw(fmachip.name) +#let zerochip = load_chip("src/fext_zero.toml", config) +#let zero = raw(zerochip.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 offer an arithmetic black box, consisting of the *TODO* chips, +Our approach is to offer an arithmetic black box, consisting of the #fma and #zero 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. @@ -73,3 +75,20 @@ We express this chip using #nr_variables variables spanning #nr_columns columns == Padding #render_chip_padding_table(fmachip, config) + += The #zero chip + +This chip asserts that a field extension element in the ABB is zero. +It uses #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. + +== Variables + +#render_chip_variable_table(zerochip, config) + +== Constraints + +#render_constraint_table(zerochip, config) + +== Padding + +#render_chip_padding_table(zerochip, config) diff --git a/spec/src/fext_zero.toml b/spec/src/fext_zero.toml new file mode 100644 index 000000000..1351efd30 --- /dev/null +++ b/spec/src/fext_zero.toml @@ -0,0 +1,44 @@ +name = "FEXT_ZERO" +code = "FXZ" + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.input]] +name = "addr" +type = "DWordWL" +desc = "The address to assert equal to zero" +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 = [["+", 3, "d"], "addr", ["cast", 0, ["BaseField", 8]], "timestamp", 0, 0, 0] +output = ["cast", 0, ["BaseField", 8]] +multiplicity = "μ" +iter = ["d", 0, 2] + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 22], ["-", ["^", 2, 32], 1]]] + From ff4765617b656b378f4b40315cfbd252322a5174 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Wed, 22 Jul 2026 10:39:05 +0200 Subject: [PATCH 09/10] clarifications --- spec/fext.typ | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/spec/fext.typ b/spec/fext.typ index d6ba762dd..141ed8b98 100644 --- a/spec/fext.typ +++ b/spec/fext.typ @@ -22,7 +22,7 @@ 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 offer an arithmetic black box, consisting of the #fma and #zero chips, +Our approach is to offer an arithmetic black box (ABB), consisting of the #fma and #zero 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. @@ -77,8 +77,11 @@ We express this chip using #nr_variables variables spanning #nr_columns columns #render_chip_padding_table(fmachip, config) = The #zero chip +#let nr_variables = total_nr_variables(zerochip) +#let nr_columns = total_nr_instantiated_columns(zerochip, config) +#let nr_interactions = compute_nr_interactions(zerochip) -This chip asserts that a field extension element in the ABB is zero. +This chip asserts that a field extension element in the ABB, passed in the `A0` register, is zero. It uses #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. == Variables @@ -87,6 +90,8 @@ It uses #nr_variables variables spanning #nr_columns columns and #nr_interaction == Constraints +Read the field element address from the `A0` register, and then assert that the field memory reads a zero. + #render_constraint_table(zerochip, config) == Padding From 36f9f2c2f986d103f09788ef11d3b0b925de72a4 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 24 Jul 2026 12:09:08 +0200 Subject: [PATCH 10/10] Switch to using REG templates + make CI pass --- spec/src/fext_fma.toml | 20 ++++++++++---------- spec/src/fext_load.toml | 20 ++++++++++---------- spec/src/fext_zero.toml | 11 ++++++----- spec/tooling/chip.py | 4 ++-- 4 files changed, 28 insertions(+), 27 deletions(-) diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml index 8d4dc04c3..59a3211b0 100644 --- a/spec/src/fext_fma.toml +++ b/spec/src/fext_fma.toml @@ -74,19 +74,19 @@ pad = 0 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] +kind = "template" +tag = "REG" +input = [["+", 10, "i"], ["idx", "input_addrs", "i"], "timestamp"] +output = ["idx", "input_addrs", "i"] iter = ["i", 0, 2] -multiplicity = "μ" +cond = "μ" [[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 = "μ" +kind = "template" +tag = "REG" +input = [13, "output_addr", "timestamp"] +output = "output_addr" +cond = "μ" [[constraints.all]] kind = "interaction" diff --git a/spec/src/fext_load.toml b/spec/src/fext_load.toml index 80c247972..9b98e9387 100644 --- a/spec/src/fext_load.toml +++ b/spec/src/fext_load.toml @@ -29,18 +29,18 @@ pad = 0 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 = "μ" +kind = "template" +tag = "REG" +input = [10, "addr", "timestamp"] +output = "addr" +cond = "μ" [[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 = "μ" +kind = "template" +tag = "REG" +input = [["+", 11, "i"], ["idx", "coeffs", "i"], "timestamp"] +output = ["idx", "coeffs", "i"] +cond = "μ" iter = ["i", 0, 2] [[constraints.all]] diff --git a/spec/src/fext_zero.toml b/spec/src/fext_zero.toml index 1351efd30..bc5098b83 100644 --- a/spec/src/fext_zero.toml +++ b/spec/src/fext_zero.toml @@ -23,11 +23,11 @@ pad = 0 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 = "μ" +kind = "template" +tag = "REG" +input = [10, "addr", "timestamp"] +output = "addr" +cond = "μ" [[constraints.all]] kind = "interaction" @@ -41,4 +41,5 @@ iter = ["d", 0, 2] kind = "interaction" tag = "ECALL" input = ["timestamp", ["arr", ["-", ["^", 2, 32], 22], ["-", ["^", 2, 32], 1]]] +multiplicity = "μ" diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index f3e5b58b6..d8e47c680 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -811,7 +811,7 @@ class Assumption: iters: list[Iter] def __init__(self, config: Config, data: dict): - assert_no_unexpected(data, set(self.__annotations__.keys()) | {"iter", "iters", "ref"}) + assert_no_unexpected(data, set(type(self).__annotations__.keys()) | {"iter", "iters", "ref"}) self.desc = data["desc"] self.iters = iters_of(data, config) @@ -824,7 +824,7 @@ class ArithConstraint: iters: list[Iter] def __init__(self, config: Config, data: dict): - assert_no_unexpected(data, set(self.__annotations__.keys()) | {"kind", "ref", "iter", "iters"}) + assert_no_unexpected(data, set(type(self).__annotations__.keys()) | {"kind", "ref", "iter", "iters"}) assert data["kind"] == "arith" self.constraint = data["constraint"] reporter.asserts(