spec: IS_WH

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`. 

spec/chapters/is_wh.typ

@@ -0,0 +1,52 @@
+#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_wh.toml", config)
+#let is_wh = raw(chip.name)
+
+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, 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.
+
+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`.
+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 #is_wh 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)
+

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")
 
@@ -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_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.

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

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

spec/meta.typ

@@ -36,7 +36,8 @@
       ("mul", [`MUL` chip], <mul>),
       ("dvrm", [`DVRM` chip], <dvrm>),
       ("bitwise", [`BITWISE` chips], <bitwise>),
-      ("bytewise", [`BYTEWISE` chip], <bytewise>)
+      ("bytewise", [`BYTEWISE` chip], <bytewise>),
+      ("is_wh", [`IS_WH`], <is-wh>),
     )),
     ("MEMORY", (
       ("memw", [`MEMW` chip], <memw>),

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]]
+iter = ["i", 0, 3]
 multiplicity = "μ"
-ref = "ec:c:range_addr_xG"
+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]]
+iter = ["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]]
+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]]
+iter = ["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]]
+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]]
+iter = ["i", 0, 3]
 multiplicity = "μ"
-ref = "ec:c:range_addr_xR"
+ref = "ec:c:range_addr_xR_hi"
 
 [[constraints.write_xR]]
 kind = "template"

spec/src/is_wh.toml

@@ -0,0 +1,31 @@
+name = "IS_WH"
+
+[[variables.input]]
+name = "value"
+type = ["Half", 3]
+desc = "`Word`-`Half` pair 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 = "is_wh:c:range_value"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "IS_WH"
+input = [["+", ["idx", "value", 1], ["*", ["^", 2, 16], ["idx", "value", 2]]], ["idx", "value", 0]]
+multiplicity = ["-", "μ"]
+ref = "is_wh:c:is_wh"

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_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 = "μ"
-ref = "keccak:c:range_state_ptr"
+ref = "keccak:c:range_state_ptr_hi"
 
 [[constraints.mem]]
 kind = "interaction"

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]]
+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 = "μ"
+iter = ["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], ["j", 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 = "μ"
+iter = ["i", 0, 3]
 
 [[constraints.memory]]
 kind = "template"

spec/src/signatures.toml

@@ -170,6 +170,12 @@ tag = "IS_B20"
 kind = "interaction"
 input = ["B20"]
 
+# IS_WH[X, Y]
+[[signatures]]
+tag = "IS_WH"
+kind = "interaction"
+input = ["Word", "Half"]
+
 # HWSL[res; X, shift]
 [[signatures]]
 tag = "HWSL"