From 315842b2a74d71641f2b6e28b6375c29ee707199 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 22 Sep 2026 12:00:58 +0200 Subject: [PATCH 1/5] spec/b48: introduce is_b48 --- spec/chapters/is_b48.typ | 50 ++++++++++++++++++++++++++++++++++++++++ spec/chapters/keccak.typ | 2 +- spec/chapters/sha256.typ | 4 +++- spec/chapters/shift.typ | 2 +- spec/meta.typ | 1 + spec/src/ecsm.toml | 48 ++++++++++++++++++++++++++++---------- spec/src/is_b48.toml | 31 +++++++++++++++++++++++++ spec/src/keccak.toml | 16 +++++++++---- spec/src/sha256.toml | 26 ++++++++++++++++----- spec/src/signatures.toml | 6 +++++ 10 files changed, 161 insertions(+), 25 deletions(-) create mode 100644 spec/chapters/is_b48.typ create mode 100644 spec/src/is_b48.toml diff --git a/spec/chapters/is_b48.typ b/spec/chapters/is_b48.typ new file mode 100644 index 000000000..760f13b62 --- /dev/null +++ b/spec/chapters/is_b48.typ @@ -0,0 +1,50 @@ +#import "/meta.typ": 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, +) + +#let config = load_config() +#let chip = load_chip("src/is_b48.toml", config) +#let b48 = raw(chip.name) + +Several `ECALL` chips load/write vast amounts of data from/to memory as part of their execution. +These memory interactions operate on at most eight bytes at a time. +For each of these interactions, the address of the memory section being accessed +has to be stored on the chip in some way. +Given that many of these loads/writes operate on contiguous memory, these address +values typically only differ in their lowest limb. +Despite virtually always being the same, the values of the upper limbs still need to +be range checked. + +To reduce range-checking pressure on these chips, this #b48 chip is introduced. +Rather than range checking all 4 `Half` limbs, several chips now only check the +bottom limb, and defer the check for the top three limbs (=48 bits) to this chip. +With several range checks for the same 48 bits coming in, the overhead incurred +on this chip is limited. +As a bonus, the calling chips can now often represent an address with a +`DWordWHH` rather than a `DWordHL`, saving a column as a result. + += Variables +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) + +The #b48 chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: +#render_chip_variable_table(chip, config) + += Constraints +#render_constraint_table(chip, config, groups: "all") + += Padding + +The table can be padded to the next power of two with the following value assignments: + +#render_chip_padding_table(chip, config) + diff --git a/spec/chapters/keccak.typ b/spec/chapters/keccak.typ index 8b918fd7e..3adf91b9c 100644 --- a/spec/chapters/keccak.typ +++ b/spec/chapters/keccak.typ @@ -39,7 +39,7 @@ The chip therefore contributes the following interaction to the lookup-argument: #render_constraint_table(chip, config, groups: "output") The address containing the state to be permuted is passed in as argument `A0 = x10`. -The following constraints describe that this address is read into `state_ptr[0][0]` (@keccak:c:read_state_ptr), from which full `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr); @keccak:c:range_state_ptr is included to satisfy @add:a:lhs respectively @add:a:sum. +The following constraints describe that this address is read into `state_ptr[0][0]` (@keccak:c:read_state_ptr), from which full `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr); @keccak:c:range_state_ptr_lo and @keccak:c:range_state_ptr_hi are included to satisfy @add:a:lhs respectively @add:a:sum. The state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccak:c:load_store_state). #render_constraint_table(chip, config, groups: "mem") diff --git a/spec/chapters/sha256.typ b/spec/chapters/sha256.typ index f9520ddb4..dab7b78b8 100644 --- a/spec/chapters/sha256.typ +++ b/spec/chapters/sha256.typ @@ -7,6 +7,7 @@ render_constraint_table, render_chip_assumptions, render_chip_padding_table, + compute_nr_interactions ) #let config = load_config() @@ -39,8 +40,9 @@ Most of the structure and variable naming follows the pseudocode of the wikipedi == Columns #let nr_variables = total_nr_variables(sha256chip) #let nr_columns = total_nr_instantiated_columns(sha256chip, config) +#let nr_interactions = compute_nr_interactions(sha256chip) -The #sha256 chip leverages #nr_variables variables, spanning #nr_columns columns: +The #sha256 chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(sha256chip, config) == Constraints diff --git a/spec/chapters/shift.typ b/spec/chapters/shift.typ index 2c5840fc5..1bbd55fa5 100644 --- a/spec/chapters/shift.typ +++ b/spec/chapters/shift.typ @@ -35,7 +35,7 @@ Here, $<<$ and $>>$ denote the _logical_ left and right shift operations, while #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) -The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): +The #shift chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) = Explanation diff --git a/spec/meta.typ b/spec/meta.typ index fc6bc783b..f6cf5eef1 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -45,6 +45,7 @@ )), ("ECALLS", ( ("about_ecalls", [About `ECALL`], ), + ("is_b48", [`IS_B48`], ), ("halt", [`HALT` chip], ), ("commit", [`COMMIT` chip], ), ("sha256", [`SHA256` accelerator], ), diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index 226c61816..9be953539 100644 --- a/spec/src/ecsm.toml +++ b/spec/src/ecsm.toml @@ -8,19 +8,19 @@ pad = 0 [[variables.input]] name = "addr_xG" -type = ["DWordHL", 4] +type = ["DWordWHH", 4] desc = "address at which `x`-coordinate of start point `G` is stored" pad = 0 [[variables.input]] name = "addr_k" -type = ["DWordHL", 4] +type = ["DWordWHH", 4] desc = "address at which scalar `k` is stored" pad = 0 [[variables.input]] name = "addr_xR" -type = ["DWordHL", 4] +type = ["DWordWHH", 4] desc = "address to which the `x`-coordinate of result point `R` is to be written" pad = 0 @@ -267,10 +267,18 @@ ref = "ec:c:read_addr_xG" [[constraints.read_xG]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", "addr_xG", "i"], "j"]] -iters = [["i", 0, 3], ["j", 0, 3]] +input = [["idx", ["idx", "addr_xG", "i"], 0]] +iters = [["i", 0, 3]] multiplicity = "μ" -ref = "ec:c:range_addr_xG" +ref = "ec:c:range_addr_xG_lo" + +[[constraints.read_xG]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", "addr_xG", "i"], 2], ["idx", ["idx", "addr_xG", "i"], 1]] +iters = [["i", 0, 3]] +multiplicity = "μ" +ref = "ec:c:range_addr_xG_hi" [[constraints.read_xG]] kind = "template" @@ -488,10 +496,18 @@ ref = "ec:c:read_addr_k" [[constraints.verify_k]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", "addr_k", "i"], "j"]] -iters = [["i", 0, 3], ["j", 0, 3]] +input = [["idx", ["idx", "addr_k", "i"], 0]] +iters = [["i", 0, 3]] +multiplicity = "μ" +ref = "ec:c:range_addr_k_lo" + +[[constraints.verify_k]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", "addr_k", "i"], 2], ["idx", ["idx", "addr_k", "i"], 1]] +iters = [["i", 0, 3]] multiplicity = "μ" -ref = "ec:c:range_addr_k" +ref = "ec:c:range_addr_k_hi" [[constraints.verify_k]] kind = "template" @@ -649,10 +665,18 @@ ref = "ec:c:load_addr_xR" [[constraints.write_xR]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", "addr_xR", "i"], "j"]] -iters = [["i", 0, 3], ["j", 0, 3]] +input = [["idx", ["idx", "addr_xR", "i"], 0]] +iters = [["i", 0, 3]] +multiplicity = "μ" +ref = "ec:c:range_addr_xR_lo" + +[[constraints.write_xR]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", "addr_xR", "i"], 2], ["idx", ["idx", "addr_xR", "i"], 1]] +iters = [["i", 0, 3]] multiplicity = "μ" -ref = "ec:c:range_addr_xR" +ref = "ec:c:range_addr_xR_hi" [[constraints.write_xR]] kind = "template" diff --git a/spec/src/is_b48.toml b/spec/src/is_b48.toml new file mode 100644 index 000000000..38ee81086 --- /dev/null +++ b/spec/src/is_b48.toml @@ -0,0 +1,31 @@ +name = "IS_B48" + +[[variables.input]] +name = "value" +type = ["Half", 3] +desc = "`B48` being range checked" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "BaseField" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "value", "i"]] +iter = ["i", 0, 2] +multiplicity = "μ" +ref = "b48:c:range_value" + +[[constraints.all]] +kind = "interaction" +tag = "IS_B48" +input = [["+", ["idx", "value", 1], ["*", ["^", 2, 16], ["idx", "value", 2]]], ["idx", "value", 0]] +multiplicity = ["-", "μ"] +ref = "b48:c:b48" \ No newline at end of file diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index d2cc8bb5c..99afb76c5 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -21,7 +21,7 @@ pad = 0 [[variables.auxiliary]] name = "state_ptr" -type = [["DWordHL", 5], 5] +type = [["DWordWHH", 5], 5] desc = "memory addresses storing the entire state" pad = ["*", 8, ["arr", ["arr", 0, 1, 2, 3, 4], @@ -69,10 +69,18 @@ ref = "keccak:c:state_ptr" [[constraints.mem]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], "z"]] -iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]] +input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 0]] +iters = [["x", 0, 4], ["y", 0, 4]] +multiplicity = "μ" +ref = "keccak:c:range_state_ptr_lo" + +[[constraints.mem]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 2], ["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 1]] +iters = [["x", 0, 4], ["y", 0, 4]] multiplicity = "μ" -ref = "keccak:c:range_state_ptr" +ref = "keccak:c:range_state_ptr_hi" [[constraints.mem]] kind = "interaction" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index ba7ad43d5..404e5e242 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -15,7 +15,7 @@ pad = 0 [[variables.input]] name = "h_addr" -type = ["DWordHL", 4] +type = ["DWordWHH", 4] desc = "The addresses of the doublewords of `h`" pad = ["arr", 0, 8, 16, 24] @@ -27,7 +27,7 @@ pad = 0 [[variables.input]] name = "m_addr" -type = ["DWordHL", 8] +type = ["DWordWHH", 8] desc = "The addresses of the doublewords of `m`" pad = ["arr", 0, 8, 16, 24, 32, 40, 48, 56] @@ -63,9 +63,16 @@ cond = "μ" [[constraints.memory]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", "m_addr", "i"], "j"]] +input = [["idx", ["idx", "m_addr", "i"], 0]] multiplicity = "μ" -iters = [["i", 0, 7], ["j", 0, 3]] +iters = [["i", 0, 7]] + +[[constraints.memory]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", "m_addr", "i"], 2], ["idx", ["idx", "m_addr", "i"], 1]] +multiplicity = "μ" +iters = [["i", 0, 7]] [[constraints.memory]] kind = "template" @@ -110,9 +117,16 @@ cond = "μ" [[constraints.memory]] kind = "interaction" tag = "IS_HALF" -input = [["idx", ["idx", "h_addr", "i"], "j"]] +input = [["idx", ["idx", "h_addr", "i"], 0]] +multiplicity = "μ" +iters = [["i", 0, 3]] + +[[constraints.memory]] +kind = "interaction" +tag = "IS_B48" +input = [["idx", ["idx", "h_addr", "i"], 2], ["idx", ["idx", "h_addr", "i"], 1]] multiplicity = "μ" -iters = [["i", 0, 3], ["j", 0, 3]] +iters = [["i", 0, 3]] [[constraints.memory]] kind = "template" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index bdc85f9bf..7c5a3b5d5 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -170,6 +170,12 @@ tag = "IS_B20" kind = "interaction" input = ["B20"] +# IS_B48[X, Y] +[[signatures]] +tag = "IS_B48" +kind = "interaction" +input = ["Word", "Half"] + # HWSL[res; X, shift] [[signatures]] tag = "HWSL" From f824964bb70d312a2ec841b7501712225134956b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 28 Sep 2026 09:51:44 +0200 Subject: [PATCH 2/5] address impacted optimization notes --- spec/chapters/ecsm.typ | 6 +++--- spec/chapters/keccak.typ | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/chapters/ecsm.typ b/spec/chapters/ecsm.typ index 210c418ac..21aa93087 100644 --- a/spec/chapters/ecsm.typ +++ b/spec/chapters/ecsm.typ @@ -367,9 +367,9 @@ $ - it would be possible to perform a 24-bit range-check lookup, - one could set up a 24-bit range-check table. This could be as narrow as two columns. - have some hybrid version, where there is a native lookup table for x-bits, and a dynamic table for outliers (high carries are not encountered frequently). -- `addr_xG[0]`, `addr_k[0]` and `addr_xR[0]` could be `DWordWL`s rather than `HL`s. - We use `HL`s as conventient notation. - This modification saves 6 columns. +- `addr_xG[0]`, `addr_k[0]` and `addr_xR[0]` could be `DWordWL`s rather than `WHH`s. + We use `WHH`s as conventient notation. + This modification saves 3 columns. - the design of these chip is generic, and makes no assumptions on the parameters $a$, $b$, $p$ and $N$. It might be possible to arrive at more compact design by making some assumptions on these values. - Constraints @ec:c:c1_0 and @ec:c:c1_i can be simplified to degree-2 constraints by padding `q1` to `p` rather than `0`. diff --git a/spec/chapters/keccak.typ b/spec/chapters/keccak.typ index 3adf91b9c..df65669d2 100644 --- a/spec/chapters/keccak.typ +++ b/spec/chapters/keccak.typ @@ -104,7 +104,7 @@ Lastly, the round chip contributes the following interactions to the lookup: == Notes/potential optimizations - one does not have to range check `state_ptr[0][0]` since it is read from memory. Moreover, it could be represented as a `DWordWL`. - All this would save 2 columns and 4 `IS_HALF` checks. + This would save one column, one `IS_HALF` check and one `IS_B48` check. - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - when the output of `HWSL` are `Byte`s mapped as `Half`s, we find that out of every four output bytes, at least one is zero. Since `rnc` is constant, @keccak:c:rho_rotation makes those zero-bytes show up in `rot_left` and `rot_right` at constant locations. From 74b7a2f9ed3483c1902412db3eea73e68a74063f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 28 Sep 2026 11:58:00 +0200 Subject: [PATCH 3/5] incorporate feedback --- spec/chapters/{is_b48.typ => is_wh.typ} | 26 +++++++++++++------------ spec/chapters/keccak.typ | 2 +- spec/meta.typ | 4 ++-- spec/src/ecsm.toml | 6 +++--- spec/src/{is_b48.toml => is_wh.toml} | 10 +++++----- spec/src/keccak.toml | 2 +- spec/src/sha256.toml | 4 ++-- spec/src/signatures.toml | 4 ++-- 8 files changed, 30 insertions(+), 28 deletions(-) rename spec/chapters/{is_b48.typ => is_wh.typ} (54%) rename spec/src/{is_b48.toml => is_wh.toml} (79%) diff --git a/spec/chapters/is_b48.typ b/spec/chapters/is_wh.typ similarity index 54% rename from spec/chapters/is_b48.typ rename to spec/chapters/is_wh.typ index 760f13b62..a1bf4df91 100644 --- a/spec/chapters/is_b48.typ +++ b/spec/chapters/is_wh.typ @@ -11,32 +11,34 @@ ) #let config = load_config() -#let chip = load_chip("src/is_b48.toml", config) -#let b48 = raw(chip.name) +#let chip = load_chip("src/is_wh.toml", config) +#let is_wh = raw(chip.name) -Several `ECALL` chips load/write vast amounts of data from/to memory as part of their execution. -These memory interactions operate on at most eight bytes at a time. +Several chips load/write vast amounts of data from/to memory as part of their execution. +This quickly involves many memory interactions, as each interaction operates on +at most eight bytes at a time. For each of these interactions, the address of the memory section being accessed has to be stored on the chip in some way. Given that many of these loads/writes operate on contiguous memory, these address -values typically only differ in their lowest limb. -Despite virtually always being the same, the values of the upper limbs still need to -be range checked. +values typically only differ in their lowest limb, but exceptions exist. +As a result of these exceptions, the values of the upper limbs still need to +be range checked for every single address. -To reduce range-checking pressure on these chips, this #b48 chip is introduced. -Rather than range checking all 4 `Half` limbs, several chips now only check the -bottom limb, and defer the check for the top three limbs (=48 bits) to this chip. +This #is_wh is introduced to reduce the range-checking pressure on these chips. +Rather than range checking all 64 bits locally, chips now only need to check the +bottom `Half` limb, and defer the check for the top 48 bits to this chip. With several range checks for the same 48 bits coming in, the overhead incurred on this chip is limited. As a bonus, the calling chips can now often represent an address with a -`DWordWHH` rather than a `DWordHL`, saving a column as a result. +`DWordWHH` rather than a `DWordHL`. +Hence, why the input of this chip are `Word`-`Half` pairs rather than `Half` triples. = Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) -The #b48 chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: +The #is_wh chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: #render_chip_variable_table(chip, config) = Constraints diff --git a/spec/chapters/keccak.typ b/spec/chapters/keccak.typ index df65669d2..f860d8933 100644 --- a/spec/chapters/keccak.typ +++ b/spec/chapters/keccak.typ @@ -104,7 +104,7 @@ Lastly, the round chip contributes the following interactions to the lookup: == Notes/potential optimizations - one does not have to range check `state_ptr[0][0]` since it is read from memory. Moreover, it could be represented as a `DWordWL`. - This would save one column, one `IS_HALF` check and one `IS_B48` check. + This would save one column, one `IS_HALF` check and one `IS_WH` check. - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions. - when the output of `HWSL` are `Byte`s mapped as `Half`s, we find that out of every four output bytes, at least one is zero. Since `rnc` is constant, @keccak:c:rho_rotation makes those zero-bytes show up in `rot_left` and `rot_right` at constant locations. diff --git a/spec/meta.typ b/spec/meta.typ index f6cf5eef1..68fe24ba4 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -36,7 +36,8 @@ ("mul", [`MUL` chip], ), ("dvrm", [`DVRM` chip], ), ("bitwise", [`BITWISE` chips], ), - ("bytewise", [`BYTEWISE` chip], ) + ("bytewise", [`BYTEWISE` chip], ), + ("is_wh", [`IS_WH`], ), )), ("MEMORY", ( ("memw", [`MEMW` chip], ), @@ -45,7 +46,6 @@ )), ("ECALLS", ( ("about_ecalls", [About `ECALL`], ), - ("is_b48", [`IS_B48`], ), ("halt", [`HALT` chip], ), ("commit", [`COMMIT` chip], ), ("sha256", [`SHA256` accelerator], ), diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index 9be953539..993060e2a 100644 --- a/spec/src/ecsm.toml +++ b/spec/src/ecsm.toml @@ -274,7 +274,7 @@ ref = "ec:c:range_addr_xG_lo" [[constraints.read_xG]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", "addr_xG", "i"], 2], ["idx", ["idx", "addr_xG", "i"], 1]] iters = [["i", 0, 3]] multiplicity = "μ" @@ -503,7 +503,7 @@ ref = "ec:c:range_addr_k_lo" [[constraints.verify_k]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", "addr_k", "i"], 2], ["idx", ["idx", "addr_k", "i"], 1]] iters = [["i", 0, 3]] multiplicity = "μ" @@ -672,7 +672,7 @@ ref = "ec:c:range_addr_xR_lo" [[constraints.write_xR]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", "addr_xR", "i"], 2], ["idx", ["idx", "addr_xR", "i"], 1]] iters = [["i", 0, 3]] multiplicity = "μ" diff --git a/spec/src/is_b48.toml b/spec/src/is_wh.toml similarity index 79% rename from spec/src/is_b48.toml rename to spec/src/is_wh.toml index 38ee81086..43bc60ab2 100644 --- a/spec/src/is_b48.toml +++ b/spec/src/is_wh.toml @@ -1,9 +1,9 @@ -name = "IS_B48" +name = "IS_WH" [[variables.input]] name = "value" type = ["Half", 3] -desc = "`B48` being range checked" +desc = "`Word`-`Half` pair being range checked" pad = 0 [[variables.multiplicity]] @@ -21,11 +21,11 @@ tag = "IS_HALF" input = [["idx", "value", "i"]] iter = ["i", 0, 2] multiplicity = "μ" -ref = "b48:c:range_value" +ref = "is_wh:c:range_value" [[constraints.all]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["+", ["idx", "value", 1], ["*", ["^", 2, 16], ["idx", "value", 2]]], ["idx", "value", 0]] multiplicity = ["-", "μ"] -ref = "b48:c:b48" \ No newline at end of file +ref = "is_wh:c:is_wh" \ No newline at end of file diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 99afb76c5..3ea3e0422 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -76,7 +76,7 @@ ref = "keccak:c:range_state_ptr_lo" [[constraints.mem]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 2], ["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 1]] iters = [["x", 0, 4], ["y", 0, 4]] multiplicity = "μ" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 404e5e242..861b69825 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -69,7 +69,7 @@ iters = [["i", 0, 7]] [[constraints.memory]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", "m_addr", "i"], 2], ["idx", ["idx", "m_addr", "i"], 1]] multiplicity = "μ" iters = [["i", 0, 7]] @@ -123,7 +123,7 @@ iters = [["i", 0, 3]] [[constraints.memory]] kind = "interaction" -tag = "IS_B48" +tag = "IS_WH" input = [["idx", ["idx", "h_addr", "i"], 2], ["idx", ["idx", "h_addr", "i"], 1]] multiplicity = "μ" iters = [["i", 0, 3]] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 7c5a3b5d5..160dbed14 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -170,9 +170,9 @@ tag = "IS_B20" kind = "interaction" input = ["B20"] -# IS_B48[X, Y] +# IS_WH[X, Y] [[signatures]] -tag = "IS_B48" +tag = "IS_WH" kind = "interaction" input = ["Word", "Half"] From 20d12d4c06d69189a9c8787ac65cf823ab74da1a Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 29 Sep 2026 08:16:42 +0200 Subject: [PATCH 4/5] Fix iters Co-authored-by: Robin Jadoul --- spec/src/ecsm.toml | 12 ++++++------ spec/src/sha256.toml | 8 ++++---- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index 993060e2a..d805b24d6 100644 --- a/spec/src/ecsm.toml +++ b/spec/src/ecsm.toml @@ -268,7 +268,7 @@ ref = "ec:c:read_addr_xG" kind = "interaction" tag = "IS_HALF" input = [["idx", ["idx", "addr_xG", "i"], 0]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_xG_lo" @@ -276,7 +276,7 @@ ref = "ec:c:range_addr_xG_lo" kind = "interaction" tag = "IS_WH" input = [["idx", ["idx", "addr_xG", "i"], 2], ["idx", ["idx", "addr_xG", "i"], 1]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_xG_hi" @@ -497,7 +497,7 @@ ref = "ec:c:read_addr_k" kind = "interaction" tag = "IS_HALF" input = [["idx", ["idx", "addr_k", "i"], 0]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_k_lo" @@ -505,7 +505,7 @@ ref = "ec:c:range_addr_k_lo" kind = "interaction" tag = "IS_WH" input = [["idx", ["idx", "addr_k", "i"], 2], ["idx", ["idx", "addr_k", "i"], 1]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_k_hi" @@ -666,7 +666,7 @@ ref = "ec:c:load_addr_xR" kind = "interaction" tag = "IS_HALF" input = [["idx", ["idx", "addr_xR", "i"], 0]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_xR_lo" @@ -674,7 +674,7 @@ ref = "ec:c:range_addr_xR_lo" kind = "interaction" tag = "IS_WH" input = [["idx", ["idx", "addr_xR", "i"], 2], ["idx", ["idx", "addr_xR", "i"], 1]] -iters = [["i", 0, 3]] +iter = ["i", 0, 3] multiplicity = "μ" ref = "ec:c:range_addr_xR_hi" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 861b69825..367aa1270 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -65,14 +65,14 @@ kind = "interaction" tag = "IS_HALF" input = [["idx", ["idx", "m_addr", "i"], 0]] multiplicity = "μ" -iters = [["i", 0, 7]] +iter = ["i", 0, 7] [[constraints.memory]] kind = "interaction" tag = "IS_WH" input = [["idx", ["idx", "m_addr", "i"], 2], ["idx", ["idx", "m_addr", "i"], 1]] multiplicity = "μ" -iters = [["i", 0, 7]] +iter = ["i", 0, 7] [[constraints.memory]] kind = "template" @@ -119,14 +119,14 @@ kind = "interaction" tag = "IS_HALF" input = [["idx", ["idx", "h_addr", "i"], 0]] multiplicity = "μ" -iters = [["i", 0, 3]] +iter = ["i", 0, 3] [[constraints.memory]] kind = "interaction" tag = "IS_WH" input = [["idx", ["idx", "h_addr", "i"], 2], ["idx", ["idx", "h_addr", "i"], 1]] multiplicity = "μ" -iters = [["i", 0, 3]] +iter = ["i", 0, 3] [[constraints.memory]] kind = "template" From 169b723a090d6f4b58ca528e6932811c7da9f28b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 29 Sep 2026 09:38:30 +0200 Subject: [PATCH 5/5] fix EOF --- spec/src/is_wh.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/is_wh.toml b/spec/src/is_wh.toml index 43bc60ab2..51426791f 100644 --- a/spec/src/is_wh.toml +++ b/spec/src/is_wh.toml @@ -28,4 +28,4 @@ kind = "interaction" tag = "IS_WH" input = [["+", ["idx", "value", 1], ["*", ["^", 2, 16], ["idx", "value", 2]]], ["idx", "value", 0]] multiplicity = ["-", "μ"] -ref = "is_wh:c:is_wh" \ No newline at end of file +ref = "is_wh:c:is_wh"