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/is_wh.typ b/spec/chapters/is_wh.typ new file mode 100644 index 000000000..a1bf4df91 --- /dev/null +++ b/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) + diff --git a/spec/chapters/keccak.typ b/spec/chapters/keccak.typ index 8b918fd7e..f860d8933 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") @@ -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. 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..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], ), diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index 226c61816..d805b24d6 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]] +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" diff --git a/spec/src/is_wh.toml b/spec/src/is_wh.toml new file mode 100644 index 000000000..51426791f --- /dev/null +++ b/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" diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index d2cc8bb5c..3ea3e0422 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_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" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index ba7ad43d5..367aa1270 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]] +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" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index bdc85f9bf..160dbed14 100644 --- a/spec/src/signatures.toml +++ b/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"