diff --git a/spec/memw.typ b/spec/memw.typ index b1f95a491..1c7a1e6e5 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -6,7 +6,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, - render_chip_padding_table, + render_chip_padding_table ) #let config = load_config() @@ -96,8 +96,62 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu The table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(alignedchip, config) -= Future optimization ideas += Register fast-path + +#let config = load_config() +#let register_chip = load_chip("src/memw_register.toml", config) +#let reg = raw(register_chip.name) + +The #reg chip provides a fast-path for accessing registers. +This fast-path leverages that registers ++ can be addressed using a `Byte`, rather than a full `DWord`, ++ are constantly accessed, i.e., $#`timestamp` - #`old_timestamp`$ is small, and ++ have a fixed access pattern +to achieve a footprint that is significantly smaller than both #memw and #aligned. + +Note: as a result of hard optimization, this chip can only be used for register accesses for which ++ $#`timestamp` - #`old_timestamp` in [1, 2^16]$, and ++ $#`timestamp[0]` > #`old_timestamp[0]`$ +If either of these rules does not apply to your access, you should fall back to using `MEMW_A`. + +Note moreover that this chip does not guard against misaligned register access faults: to access register with a given `address`, one must provide $2 dot #`address`$ in the lookup. + +== Columns +#let nr_variables = total_nr_variables(register_chip) +#let nr_columns = total_nr_instantiated_columns(register_chip, config) + +The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(register_chip, config) + +== Assumptions +The following range checks are assumed to be performed/enforced outside of this chip: +#render_chip_assumptions(register_chip, config) +== Constraints +Since most registers are frequently accessed, the difference between `timestamp` and `old_timestamp` is small most of the times. +Rather than storing their (nearly) identical upper limbs twice, it is instead assumed that +$#`old_timestamp[1]` = #`timestamp[1]`$; #aligned can be used for accesses where this is not the case. + +Verifying that $#`timestamp` > #`old_timestamp`$ now simplifies to verifying that $#`timestamp[0]` - #`old_timestamp[0]` > 0$. +For most accesses, this value will be small enough to fit in a `Half`. +This chip thus enforces this by means of the following constraint: +#render_constraint_table(register_chip, config, groups: "diff") + +With $#`old_timestamp`<#`timestamp`$ asserted, `old` is read from the register (@regw:c:read_old) and `val` is written back (@regw:c:write_val). +#render_constraint_table(register_chip, config, groups: "interactions") + +This chip can either just write ($#`μ_write` = 1$), or both read and write ($#`μ_read` = 1$) in the same cycle. +It must be asserted that at most one of these two options is selected: +#render_constraint_table(register_chip, config, groups: "multiplicities") + +Lastly, this chip contributes the following interactions to the logup: +#render_constraint_table(register_chip, config, groups: "output") + +== Padding +The table can be padded to the next power of two with the following value assignments: +#render_chip_padding_table(register_chip, config) + += Future optimization ideas - `MEMB` chip that does a one-byte write to remove old_timestamp from here (uncertain tradeoffs) -- Additional fast path for registers? (Always guaranteed same timestamp, alignment could be an assumption, always only two values) - Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALF` lookups may make some GKR things faster if there are known zeroes. +- For the register fast-path, one may upgrade the `IS_HALF` check to an `IS_B20` check for extended range at the cost of looking through a larger table. \ No newline at end of file diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml new file mode 100644 index 000000000..3e7cdcf28 --- /dev/null +++ b/spec/src/memw_register.toml @@ -0,0 +1,141 @@ +name = "MEMW_R" + +# Variables + +[[variables.input]] +name = "address" +type = "Byte" +desc = "address of the register being accessed" +pad = 0 + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "timestamp at which the access takes place" +pad = 0 + +[[variables.input]] +name = "val" +type = "DWordWL" +desc = "value being written to this register" +pad = 0 + +[[variables.output]] +name = "old" +type = "DWordWL" +desc = "value of this register at `old_timestamp`." +pad = 0 + +[[variables.auxiliary]] +name = "old_timestamp_lo" +type = "Word" +desc = "the lower limb of `old_timestamp`" +pad = 0 + +[[variables.virtual]] +name = "old_timestamp" +type = "DWordWL" +desc = "timestamp at which this register was last accessed" +def = ["cast", ["arr", "old_timestamp_lo", ["idx", "timestamp", 1]], "DWordWL"] + +[[variables.virtual]] +name = "μ_sum" +type = "Bit" +desc = "" +def = ["+", "μ_read", "μ_write"] + +[[variables.multiplicity]] +name = "μ_read" +type = "Bit" +desc = "Whether we are performing a read (and hence return `out`)" +pad = 0 + +[[variables.multiplicity]] +name = "μ_write" +type = "Bit" +desc = "Whether we are performing a write (and hence not return `out`)" +pad = 0 + + + +# Assumptions + +[[assumptions]] +desc = "`IS_WORD[val[i]]`" +iter = ["i", 0, 1] +ref = "regw:a:val" + +[[assumptions]] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] +ref = "regw:a:timestamp" + +# Constraints + +[[constraint_groups]] +name = "diff" + +[[constraints.diff]] +kind = "interaction" +tag = "IS_HALF" +input = [["-", ["idx", "timestamp", 0], ["idx", "old_timestamp", 0], 1]] +multiplicity = "μ_sum" +ref = "regw:c:diff" + + +[[constraint_groups]] +name = "multiplicities" + +[[constraints.multiplicities]] +kind = "template" +tag = "IS_BIT" +input = ["μ_read"] +ref = "regw:c:μ_read_is_bit" + +[[constraints.multiplicities]] +kind = "template" +tag = "IS_BIT" +input = ["μ_write"] +ref = "regw:c:μ_write_is_bit" + +[[constraints.multiplicities]] +kind = "template" +tag = "IS_BIT" +input = ["μ_sum"] +ref = "regw:c:μ_sum_is_bit" + +[[constraint_groups]] +name = "interactions" + +[[constraints.interactions]] +kind = "interaction" +tag = "memory" +input = [1, ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "old_timestamp", ["idx", "old", "i"]] +iter = ["i", 0, 1] +multiplicity = "μ_sum" +ref = "regw:c:read_old" + +[[constraints.interactions]] +kind = "interaction" +tag = "memory" +input = [1, ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "timestamp", ["idx", "val", "i"]] +iter = ["i", 0, 1] +multiplicity = ["-", "μ_sum"] +ref = "regw:c:write_val" + + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "MEMW" +input = [1, ["arr", ["cast", ["*", 2, "address"], "Word"], 0], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +output = ["arr", ["idx", "old", 0], ["idx", "old", 1], 0, 0, 0, 0, 0, 0] +multiplicity = ["-", "μ_read"] + +[[constraints.output]] +kind = "interaction" +tag = "MEMW" +input = [1, ["arr", ["cast", ["*", 2, "address"], "Word"], 0], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +multiplicity = ["-", "μ_write"]