From 45067c27dde045a3639f748c27ea89834d53db10 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 25 Sep 2026 11:08:06 +0200 Subject: [PATCH 1/2] introduce `is_whh` template --- spec/chapters/is_whh.typ | 31 +++++++++++++++++++++++++++++++ spec/meta.typ | 1 + spec/src/is_whh.toml | 28 ++++++++++++++++++++++++++++ spec/src/signatures.toml | 7 +++++++ 4 files changed, 67 insertions(+) create mode 100644 spec/chapters/is_whh.typ create mode 100644 spec/src/is_whh.toml diff --git a/spec/chapters/is_whh.typ b/spec/chapters/is_whh.typ new file mode 100644 index 000000000..2e12032b4 --- /dev/null +++ b/spec/chapters/is_whh.typ @@ -0,0 +1,31 @@ +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + compute_nr_interactions, + render_chip_variable_table, + render_constraint_table, + set_nr_interactions, + total_nr_instantiated_columns, + total_nr_variables, +) + +#let config = load_config() +#let chip = load_chip("src/is_whh.toml", config) + +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) +#let nr_interactions = compute_nr_interactions(chip) + +#let is_whh = raw(chip.name) + +#is_whh is a constraint template that is used to assert that a variable of three columns +consists of a `Word` limb and two `Half` limbs. +Using this template is space-reducing when a chip calls it several times, +where for each call it is expected that the `Word` limb and the first `Half` +limb remain constant. + += Variables +The #is_whh 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) + += Constraints +#render_constraint_table(chip, config) diff --git a/spec/meta.typ b/spec/meta.typ index 68fe24ba4..35643597c 100644 --- a/spec/meta.typ +++ b/spec/meta.typ @@ -18,6 +18,7 @@ ("TEMPLATES", ( ("is_bit", [`IS_BIT` template], ), ("is_byte", [`IS_BYTE` template], ), + ("is_whh", [`IS_WHH` template], ), ("sign", [`SIGN` template], ), ("add", [`ADD`/`SUB` template], ), ("neg", [`NEG` template], ), diff --git a/spec/src/is_whh.toml b/spec/src/is_whh.toml new file mode 100644 index 000000000..f00392ddb --- /dev/null +++ b/spec/src/is_whh.toml @@ -0,0 +1,28 @@ +name = "IS_WHH" +code = "WHH" + +[[variables.condition]] +name = "cond" +type = "BaseField" +desc = "the multiplicity with which to apply the interactions" + +[[variables.input]] +name = "double_word" +type = "DWordWHH" +desc = "the double word being range checked" + + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "interaction" +tag = "IS_WH" +input = [["idx", "double_word", 2], ["idx", "double_word", 1]] +multiplicity = "cond" + +[[constraints.all]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "double_word", 0]] +multiplicity = "cond" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 160dbed14..11db2fff9 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -176,6 +176,13 @@ tag = "IS_WH" kind = "interaction" input = ["Word", "Half"] +# IS_WHH[X, Y] +[[signatures]] +tag = "IS_WHH" +kind = "template" +input = ["DWordWHH"] +cond = "BaseField" + # HWSL[res; X, shift] [[signatures]] tag = "HWSL" From 6f5966768b3babc476c37e1cf6ba72e133a7151a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 1 Oct 2026 11:05:18 +0200 Subject: [PATCH 2/2] apply is_whh template --- spec/chapters/keccak.typ | 2 +- spec/src/ecsm.toml | 54 +++++++++++----------------------------- spec/src/keccak.toml | 18 ++++---------- spec/src/sha256.toml | 30 ++++++---------------- 4 files changed, 29 insertions(+), 75 deletions(-) diff --git a/spec/chapters/keccak.typ b/spec/chapters/keccak.typ index f860d8933..3b892f9ca 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_lo and @keccak:c:range_state_ptr_hi are 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 is 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/src/ecsm.toml b/spec/src/ecsm.toml index d805b24d6..85c2668fc 100644 --- a/spec/src/ecsm.toml +++ b/spec/src/ecsm.toml @@ -265,20 +265,12 @@ cond = "μ" ref = "ec:c:read_addr_xG" [[constraints.read_xG]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", ["idx", "addr_xG", "i"], 0]] -iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_xG_lo" - -[[constraints.read_xG]] -kind = "interaction" -tag = "IS_WH" -input = [["idx", ["idx", "addr_xG", "i"], 2], ["idx", ["idx", "addr_xG", "i"], 1]] +kind = "template" +tag = "IS_WHH" +input = [["idx", "addr_xG", "i"]] iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_xG_hi" +cond = "μ" +ref = "ec:c:range_addr_xG" [[constraints.read_xG]] kind = "template" @@ -494,20 +486,12 @@ cond = "μ" ref = "ec:c:read_addr_k" [[constraints.verify_k]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", ["idx", "addr_k", "i"], 0]] -iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_k_lo" - -[[constraints.verify_k]] -kind = "interaction" -tag = "IS_WH" -input = [["idx", ["idx", "addr_k", "i"], 2], ["idx", ["idx", "addr_k", "i"], 1]] +kind = "template" +tag = "IS_WHH" +input = [["idx", "addr_k", "i"]] iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_k_hi" +cond = "μ" +ref = "ec:c:range_addr_k" [[constraints.verify_k]] kind = "template" @@ -663,20 +647,12 @@ cond = "μ" ref = "ec:c:load_addr_xR" [[constraints.write_xR]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", ["idx", "addr_xR", "i"], 0]] -iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_xR_lo" - -[[constraints.write_xR]] -kind = "interaction" -tag = "IS_WH" -input = [["idx", ["idx", "addr_xR", "i"], 2], ["idx", ["idx", "addr_xR", "i"], 1]] +kind = "template" +tag = "IS_WHH" +input = [["idx", "addr_xR", "i"]] iter = ["i", 0, 3] -multiplicity = "μ" -ref = "ec:c:range_addr_xR_hi" +cond = "μ" +ref = "ec:c:range_addr_xR" [[constraints.write_xR]] kind = "template" diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 3ea3e0422..41d52b2a8 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -67,20 +67,12 @@ iters = [["x", 0, 4], ["y", 0, 4]] ref = "keccak:c:state_ptr" [[constraints.mem]] -kind = "interaction" -tag = "IS_HALF" -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_WH" -input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 2], ["idx", ["idx", ["idx", "state_ptr", "x"], "y"], 1]] +kind = "template" +tag = "IS_WHH" +input = [["idx", ["idx", "state_ptr", "x"], "y"]] iters = [["x", 0, 4], ["y", 0, 4]] -multiplicity = "μ" -ref = "keccak:c:range_state_ptr_hi" +cond = "μ" +ref = "keccak:c:range_state_ptr" [[constraints.mem]] kind = "interaction" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 367aa1270..cf369f5c0 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -61,17 +61,10 @@ output = ["cast", ["idx", "m_addr", 0], "DWordWL"] cond = "μ" [[constraints.memory]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", ["idx", "m_addr", "i"], 0]] -multiplicity = "μ" -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 = "μ" +kind = "template" +tag = "IS_WHH" +input = [["idx", "m_addr", "i"]] +cond = "μ" iter = ["i", 0, 7] [[constraints.memory]] @@ -115,17 +108,10 @@ output = ["cast", ["idx", "h_addr", 0], "DWordWL"] cond = "μ" [[constraints.memory]] -kind = "interaction" -tag = "IS_HALF" -input = [["idx", ["idx", "h_addr", "i"], 0]] -multiplicity = "μ" -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 = "μ" +kind = "template" +tag = "IS_WHH" +input = [["idx", "h_addr", "i"]] +cond = "μ" iter = ["i", 0, 3] [[constraints.memory]]