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"