spec: IS_B48

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

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

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

@@ -45,6 +45,7 @@
     )),
     ("ECALLS", (
       ("about_ecalls", [About `ECALL`], <ecall>),
+      ("is_b48", [`IS_B48`], <is-b48>),
       ("halt", [`HALT` chip], <halt>),
       ("commit", [`COMMIT` chip], <commit>),
       ("sha256", [`SHA256` accelerator], <sha256>),

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"

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"

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"

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"

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"