Skip to content

spec: Losing some MEMW weight #398

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RobinJadoul merged 1 commit into from
Mar 13, 2026
Merged

spec: Losing some MEMW weight #398

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 35 additions & 7 deletions spec/memw.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,16 +38,23 @@ we document it here, keeping the type information as a reading help.

= Constraints

We can compute the addresses for the later bytes based on a single bit each,
indicating whether adding `i` to `base_address` overflows the lower limb.
We can safely assume that additions for which this bit is not correctly set
will have either an overflow on the upper or lower word, and hence not match
any existing memory tokens, which are only initialized for correctly formatted
and range-checked doublewords (see @memory).

#render_constraint_table(chip, config, groups: "consistency")

As long as `timestamp` is properly range-checked, the presence of `old_timestamp`
in the memory argument automatically ensures appropriate range checking
(as long as no external entities provide negative multiplicities without range checking the timestamp).
This ensures the assumptions for `LT` are satisfied.

We additionally check that the address does not overflow
for more significant bytes of the access.
#render_constraint_table(chip, config, groups: "overflow")
There is no need to check that the address does not overflow,
as our address calculations are not performed modulo $2^64$ here,
and any overflow will result in an address without matching initialization.

The chip adds the following tuples to the lookup argument,
to effectuate that part of the memory argument.
Expand All @@ -56,11 +63,32 @@ to effectuate that part of the memory argument.
This chip contributes the following to the lookup argument.
#render_constraint_table(chip, config, groups: "output")

= Read-size aligned fast path

#let alignedchip = load_chip("src/memw_aligned.toml", config)
#let aligned = raw(alignedchip.name)

When a memory access happens at an address with proper alignment
(that is, enough trailing zeros) for its access size, and all accessed
elements were last accessed at the same timestamp, we can
instead use the #aligned chip to save on total column count.
The saving comes from only requiring a single old timestamp to be stored,
as well as being able to guarantee that all values of `add_limb_overflow` would be zero.
A minor extra cost is introduced in the form of a check that the alignment is indeed correct,
and the corresponding decomposition of the `base_address`.

Further logic remains essentially the same, so we briefly present the relevant tables for this chip.
#let nr_variables = total_nr_variables(alignedchip)
#let nr_columns = total_nr_instantiated_columns(alignedchip, config)

The #aligned chip only needs #nr_variables variables, expressed through #nr_columns columns.
#render_chip_column_table(alignedchip, config)
#render_chip_assumptions(alignedchip, config)
#render_constraint_table(alignedchip, config)


= Future optimization ideas

- Fast path for aligned memory access where all bytes have the same old timestamp
- MEMB chip that deals does a one-byte write to remove old_timestamp from here (uncertain tradeoffs)
- Compute `base_address[1] + 1` once and have high words of `address_add` as Words
- Improve overflow trapping somehow so we don't need `LT` (could tie into previous one by checking carry bit of the +1)
- `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.
107 changes: 21 additions & 86 deletions spec/src/memw.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,9 @@ Only the elements corresponding to the `writeN` bits are guaranteed"""
# Auxiliary

[[variables.auxiliary]]
name = "address_add"
type = ["DWordHL", 7]
desc = "`address_add[i] = base_address + i + 1`"
name = "add_limb_overflow"
type = ["Bit", 7]
desc = "Whether adding `i` to `base_address[0]` as a field element exceeds $2^32$"

[[variables.auxiliary]]
name = "old_timestamp"
Expand All @@ -71,6 +71,15 @@ type = "Bit"
desc = "writing at least 4 bytes"
def = ["+", "write4", "write8"]

[[variables.virtual]]
name = "address_add"
type = ["DWordWL", 7]
desc = "`address_add[i] = base_address + i + 1`"
def.iter = ["i", 0, 6]
def.poly = ["arr",
["+", ["idx", "base_address", 0], "i", 1, ["*", ["-", ["^", 2, 32]], ["idx", "add_limb_overflow", "i"]]],
["+", ["idx", "base_address", 1], ["idx", "add_limb_overflow", "i"]]]

[[variables.virtual]]
name = "μ_sum"
type = "Bit"
Expand Down Expand Up @@ -126,56 +135,9 @@ poly = ["*", "w2", ["not", "μ_sum"]]

[[constraints.consistency]]
kind = "template"
tag = "ADD"
input = ["base_address", ["cast", 1, "DWordWL"]]
output = ["cast", ["idx", "address_add", 0], "DWordWL"]
cond = "w2"

[[constraints.consistency]]
kind = "template"
tag = "ADD"
input = ["base_address", ["cast", ["+", "i", 1], "DWordWL"]]
output = ["cast", ["idx", "address_add", "i"], "DWordWL"]
iter = ["i", 1, 2]
cond = "w4"

[[constraints.consistency]]
kind = "template"
tag = "ADD"
input = ["base_address", ["cast", ["+", "i", 1], "DWordWL"]]
output = ["cast", ["idx", "address_add", "i"], "DWordWL"]
iter = ["i", 3, 6]
cond = "write8"

[[constraints.consistency]]
kind = "interaction"
tag = "IS_HALF"
input = [["idx", ["idx", "address_add", "i"], "j"]]
iters = [
["i", 0, 0],
["j", 0, 3],
]
multiplicity = "w2"

[[constraints.consistency]]
kind = "interaction"
tag = "IS_HALF"
input = [["idx", ["idx", "address_add", "i"], "j"]]
iters = [
["i", 1, 2],
["j", 0, 3],
]
multiplicity = "w4"

[[constraints.consistency]]
kind = "interaction"
tag = "IS_HALF"
input = [["idx", ["idx", "address_add", "i"], "j"]]
iters = [
["i", 3, 6],
["j", 0, 3],
]
multiplicity = "write8"
tag = "IS_BIT"
input = [["idx", "add_limb_overflow", "i"]]
iter = ["i", 0, 6]

[[constraints.consistency]]
kind = "interaction"
Expand Down Expand Up @@ -207,33 +169,6 @@ output = 1
iter = ["i", 4, 7]
multiplicity = "write8"


[[constraint_groups]]
name = "overflow"
prefix = "R"

[[constraints.overflow]]
kind = "interaction"
tag = "LT"
input = ["base_address", ["cast", ["idx", "address_add", 0], "DWordWL"], 0]
output = 1
multiplicity = "write2"

[[constraints.overflow]]
kind = "interaction"
tag = "LT"
input = ["base_address", ["cast", ["idx", "address_add", 2], "DWordWL"], 0]
output = 1
multiplicity = "write4"

[[constraints.overflow]]
kind = "interaction"
tag = "LT"
input = ["base_address", ["cast", ["idx", "address_add", 6], "DWordWL"], 0]
output = 1
multiplicity = "write8"


[[constraint_groups]]
name = "memory"
prefix = "M"
Expand All @@ -253,40 +188,40 @@ multiplicity = ["-", "μ_sum"]
[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", 0], "DWordWL"], ["idx", "old_timestamp", 1], ["idx", "old", 1]]
input = ["is_register", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]]
multiplicity = "w2"

[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", 0], "DWordWL"], "timestamp", ["idx", "value", 1]]
input = ["is_register", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]]
multiplicity = ["-", "w2"]

[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
multiplicity = "w4"
iter = ["i", 2, 3]

[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], "timestamp", ["idx", "value", "i"]]
input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]]
multiplicity = ["-", "w4"]
iter = ["i", 2, 3]

[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
multiplicity = "write8"
iter = ["i", 4, 7]

[[constraints.memory]]
kind = "interaction"
tag = "memory"
input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], "timestamp", ["idx", "value", "i"]]
input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]]
multiplicity = ["-", "write8"]
iter = ["i", 4, 7]

Expand Down
Loading