spec: IS_WHH template

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)

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")
 

spec/meta.typ

@@ -18,6 +18,7 @@
     ("TEMPLATES", (
       ("is_bit", [`IS_BIT` template], <isbit>),
       ("is_byte", [`IS_BYTE` template], <isbyte>),
+      ("is_whh", [`IS_WHH` template], <iswhh>),
       ("sign", [`SIGN` template], <sign>),
       ("add", [`ADD`/`SUB` template], <add>),
       ("neg", [`NEG` template], <neg>),

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"

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"

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"

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]]

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"