From f38c1c7a70c04a650335509691836a7639920445 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 09:26:35 +0100 Subject: [PATCH 01/28] spec/memw: read/write from/to -> read from/write to --- spec/src/memw.toml | 2 +- spec/src/memw_aligned.toml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index c9519e115..be8041139 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -10,7 +10,7 @@ desc = "Whether the address represents a register index" [[variables.input]] name = "base_address" type = "DWordWL" -desc = "The base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +desc = "The base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" [[variables.input]] name = "value" diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 8df912111..ddad79dae 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -10,17 +10,17 @@ desc = "Whether the address represents a register index" [[variables.input]] name = "base_address_high" type = "Word" -desc = "The high word of the base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +desc = "The high word of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" [[variables.input]] name = "base_address_mid" type = "Half" -desc = "The middle halfword of the base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +desc = "The middle halfword of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" [[variables.input]] name = "base_address_low" type = ["Byte", 2] -desc = "The low bytes of the base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is" +desc = "The low bytes of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" [[variables.input]] name = "value" From 677b166da483a77899ecdb86b8810e76b5f35f84 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 09:28:18 +0100 Subject: [PATCH 02/28] spec/memw: rename add_limb_overflow as carry --- spec/src/memw.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index be8041139..6f452b5a8 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -48,7 +48,7 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" # Auxiliary [[variables.auxiliary]] -name = "add_limb_overflow" +name = "carry" type = ["Bit", 7] desc = "Whether adding `i` to `base_address[0]` as a field element exceeds $2^32$" @@ -77,8 +77,8 @@ 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"]]] + ["+", ["idx", "base_address", 0], "i", 1, ["*", ["-", ["^", 2, 32]], ["idx", "carry", "i"]]], + ["+", ["idx", "base_address", 1], ["idx", "carry", "i"]]] [[variables.virtual]] name = "μ_sum" @@ -136,7 +136,7 @@ poly = ["*", "w2", ["not", "μ_sum"]] [[constraints.consistency]] kind = "template" tag = "IS_BIT" -input = [["idx", "add_limb_overflow", "i"]] +input = [["idx", "carry", "i"]] iter = ["i", 0, 6] [[constraints.consistency]] From ad3f093e39c976cb7f02539b859294c08277ebae Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 09:30:40 +0100 Subject: [PATCH 03/28] spec/memw: minor var desc updates --- spec/src/memw.toml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 6f452b5a8..acc03a8f0 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -10,17 +10,17 @@ desc = "Whether the address represents a register index" [[variables.input]] name = "base_address" type = "DWordWL" -desc = "The base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" +desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access" [[variables.input]] name = "value" type = ["BaseField", 8] -desc = "The values to store in memory. For regular memory, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" +desc = "The values to store in memory. For RAM, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" [[variables.input]] name = "timestamp" type = "DWordWL" -desc = "The timestamp at which this memory access is said to occur" +desc = "The timestamp at which this memory access occurs" [[variables.input]] name = "write2" @@ -50,12 +50,12 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" [[variables.auxiliary]] name = "carry" type = ["Bit", 7] -desc = "Whether adding `i` to `base_address[0]` as a field element exceeds $2^32$" +desc = "Whether `base_address[0] + i + 1` $>= 2^32$" [[variables.auxiliary]] name = "old_timestamp" type = ["DWordWL", 8] -desc = "The timestamp at which the address was last accessed" +desc = "The timestamp at which address `base_address + i` was last accessed" # Virtual From 109489b0a66db6452a61b47874b1b204bdf56439 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 09:31:00 +0100 Subject: [PATCH 04/28] spec/memw: remove superfluous minus symbol --- spec/src/memw.toml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index acc03a8f0..e6b404199 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -1,3 +1,10 @@ +# Notes: +# 1. this version is a teeny-bit more memory aligned than its predecessor: +# 0xFF..FF overflows to 0x100..00 rather than 0x00..00. +# 2. perhaps "is_register: Bit" should be replaced by "domain: BaseField", +# where it is elsewhere explained that RAM <-> domain=0 and registers <-> domain=1. +# this also opens the possibility of further memory domains (e.g. for the kernel) + name = "MEMW" # Input @@ -77,7 +84,7 @@ 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", "carry", "i"]]], + ["-", ["+", ["idx", "base_address", 0], "i", 1], ["*", ["^", 2, 32], ["idx", "carry", "i"]]], ["+", ["idx", "base_address", 1], ["idx", "carry", "i"]]] [[variables.virtual]] From 03a2338118a9875a0ab15cea49a26cf5f96ee412 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 10:07:57 +0100 Subject: [PATCH 05/28] spec/memw: update description --- spec/memw.typ | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 57907e26c..1de1e8e09 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -33,26 +33,27 @@ The `MEMW` chip is comprised of #nr_variables variables that are expressed using Our assumptions do not explicitly cover any range checks for the `is_register` and `value` columns, as these are not necessary for the correctness of this chip in isolation. -These properties are necessary for the consistency of the system as a whole, and therefore +Still, these properties are necessary for the consistency of the system as a whole, and therefore 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). +Depending on the values of `write2`, `write4` and `write8`, the addresses following `base_address` need to be constructed. +Rather than computing these in full (which would require the later addresses to be instantiated), +it suffices to know the `carry`: the bit indicating whether $#`base_address`_0 + i >= 2^32$, i.e., whether adding $i$ to `base_address` requires a carry from the lower to the upper limb. +Note that it is safe for the prover to chose these bits: additions for which this bit is not correctly set +will yield an address where either the lower or upper limb is out of bounds. +As such, the constructed address will 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). +in the memory argument automatically ensures it is appropriately range checked +(this assumes no external entities provide negative multiplicities without range checking the timestamp). This ensures the assumptions for `LT` are satisfied. -There is no need to check that the address does not overflow, +There is no need to check that the additions do not overflow, as our address calculations are not performed modulo $2^64$ here, and any overflow will result in an address without matching initialization. @@ -60,7 +61,7 @@ The chip adds the following tuples to the lookup argument, to effectuate that part of the memory argument. #render_constraint_table(chip, config, groups: "memory") -This chip contributes the following to the lookup argument. +This chip contributes the following to the lookup argument: #render_constraint_table(chip, config, groups: "output") = Read-size aligned fast path From b8fc0b7a762decae88b567eeb852deece1699fa4 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 10:15:14 +0100 Subject: [PATCH 06/28] spec/memw_a: minor optimization --- spec/src/memw_aligned.toml | 55 +++++++++++--------------------------- 1 file changed, 15 insertions(+), 40 deletions(-) diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index ddad79dae..8b6b642fc 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -8,19 +8,9 @@ type = "Bit" desc = "Whether the address represents a register index" [[variables.input]] -name = "base_address_high" -type = "Word" -desc = "The high word of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" - -[[variables.input]] -name = "base_address_mid" -type = "Half" -desc = "The middle halfword of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" - -[[variables.input]] -name = "base_address_low" -type = ["Byte", 2] -desc = "The low bytes of the base address to read from/write to, gets offset by $[0, 7]$, depending on how big the access is" +name = "base_address" +type = "DWordWHH" +desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access" [[variables.input]] name = "value" @@ -52,7 +42,7 @@ desc = "Whether to write exactly 8 values" [[variables.output]] name = "old" type = ["BaseField", 8] -desc = """The old value written at `base_address`. See `value` for information about representation. +desc = """The old value written at `base_address + i`. See `value` for information about representation. Only the elements corresponding to the `writeN` bits are guaranteed""" # Auxiliary @@ -64,14 +54,6 @@ desc = "The timestamp at which the address was last accessed" # Virtual -[[variables.virtual]] -name = "base_address" -type = "DWordWL" -desc = "Recomposing the base address from its parts" -def = {idx = "i", polys = [ - { iter = 0, poly = ["+", ["*", ["^", 2, 16], "base_address_mid"], ["*", ["^", 2, 8], ["idx", "base_address_low", 1]], ["idx", "base_address_low", 0]] }, - { iter = 1, poly = "base_address_high" }]} - [[variables.virtual]] name = "w2" type = "Bit" @@ -103,13 +85,7 @@ type = "Bit" desc = "Whether we are performing a write (and hence not return `out`)" [[assumptions]] -desc = "`IS_WORD[base_address_high]`" - -[[assumptions]] -desc = "`IS_HALF[base_address_mid]`" - -[[assumptions]] -desc = "`IS_BYTE[base_address_low[i]]`" +desc = "`IS_WORD[base_address[i]]`" iter = ["i", 0, 1] [[assumptions]] @@ -134,9 +110,8 @@ name = "consistency" [[constraints.consistency]] kind = "interaction" -tag = "AND_BYTE" -input = [["idx", "base_address_low", 0], ["+", ["*", "write2", 1], ["*", "write4", 3], ["*", "write8", 7]]] -output = 0 +tag = "IS_HALFWORD" +input = [["+", ["idx", "base_address", 0], "write2", ["*", 3, "write4"], ["*", 7, "write8"]]] multiplicity = "μ_sum" [[constraints.consistency]] @@ -163,52 +138,52 @@ prefix = "M" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", "base_address", "old_timestamp", ["idx", "old", 0]] +input = ["is_register", ["cast", "base_address", "DWordWL"], "old_timestamp", ["idx", "old", 0]] multiplicity = "μ_sum" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", "base_address", "timestamp", ["idx", "value", 0]] +input = ["is_register", ["cast", "base_address", "DWordWL"], "timestamp", ["idx", "value", 0]] multiplicity = ["-", "μ_sum"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", 1, "DWordWL"]], "old_timestamp", ["idx", "old", 1]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "old_timestamp", ["idx", "old", 1]] multiplicity = "w2" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", 1, "DWordWL"]], "timestamp", ["idx", "value", 1]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "timestamp", ["idx", "value", 1]] multiplicity = ["-", "w2"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] multiplicity = "w4" iter = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "w4"] iter = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] multiplicity = "write8" iter = ["i", 4, 7] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", "base_address", ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] +input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "write8"] iter = ["i", 4, 7] From b6b00c6544448519a40d874d69bc82c811c44909 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Wed, 18 Mar 2026 10:45:38 +0100 Subject: [PATCH 07/28] Apply suggestions from code review Co-authored-by: Robin Jadoul --- spec/src/memw_aligned.toml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 8b6b642fc..de5294fd5 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -85,9 +85,12 @@ type = "Bit" desc = "Whether we are performing a write (and hence not return `out`)" [[assumptions]] -desc = "`IS_WORD[base_address[i]]`" +desc = "`IS_HALF[base_address[i]]`" iter = ["i", 0, 1] +[[assumptions]] +desc = "`IS_WORD[base_address[2]]`" + [[assumptions]] desc = "`IS_BIT`" @@ -110,7 +113,7 @@ name = "consistency" [[constraints.consistency]] kind = "interaction" -tag = "IS_HALFWORD" +tag = "IS_HALF" input = [["+", ["idx", "base_address", 0], "write2", ["*", 3, "write4"], ["*", 7, "write8"]]] multiplicity = "μ_sum" From a099bbd77c9b4ea2dab19c086b73fc9119eedfc2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 18 Mar 2026 10:38:36 +0100 Subject: [PATCH 08/28] spec/MEMW: fix interaction typing --- spec/src/memw_aligned.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index de5294fd5..be6bb1603 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -198,12 +198,12 @@ prefix = "O" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] +input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] output = "old" multiplicity = "μ_read" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] +input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] multiplicity = "μ_write" From 448555dc8d1f21efdbc52377d4e06451d2263753 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 18 Mar 2026 10:47:41 +0100 Subject: [PATCH 09/28] spec/MEMW: drop superfluous notes --- spec/src/memw.toml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index e6b404199..4905fc5aa 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -1,10 +1,3 @@ -# Notes: -# 1. this version is a teeny-bit more memory aligned than its predecessor: -# 0xFF..FF overflows to 0x100..00 rather than 0x00..00. -# 2. perhaps "is_register: Bit" should be replaced by "domain: BaseField", -# where it is elsewhere explained that RAM <-> domain=0 and registers <-> domain=1. -# this also opens the possibility of further memory domains (e.g. for the kernel) - name = "MEMW" # Input From 4936d8c376fdfcaca3977ee85420309eeee91cdb Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 18 Mar 2026 10:55:32 +0100 Subject: [PATCH 10/28] spec/MEMW: update alignment requirement --- spec/memw.typ | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 1de1e8e09..7b0764bd0 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -69,9 +69,9 @@ This chip contributes the following to the lookup argument: #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 +When a memory access happens at an address with proper alignment for its access size +(i.e., adding the access size to `base_address`'s lowest limb does not overflow), +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. From 0e3d0f8abd5d73b63c4106e4359848748edc7e96 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 18 Mar 2026 11:04:48 +0100 Subject: [PATCH 11/28] spec/MEMW: intentionally separate carry's prose and .toml descriptions --- spec/memw.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/memw.typ b/spec/memw.typ index 7b0764bd0..f70496aa8 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -40,7 +40,7 @@ we document it here, keeping the type information as a reading help. Depending on the values of `write2`, `write4` and `write8`, the addresses following `base_address` need to be constructed. Rather than computing these in full (which would require the later addresses to be instantiated), -it suffices to know the `carry`: the bit indicating whether $#`base_address`_0 + i >= 2^32$, i.e., whether adding $i$ to `base_address` requires a carry from the lower to the upper limb. +it suffices to know the `carry`: the bit indicating whether $#`base_address`_0 + t >= 2^32$, i.e., whether adding $t in [1, 7]$ to `base_address` requires a carry from the lower to the upper limb. Note that it is safe for the prover to chose these bits: additions for which this bit is not correctly set will yield an address where either the lower or upper limb is out of bounds. As such, the constructed address will not match any existing memory tokens, From 46b9e97c1dbdd447d20be51a90a0eb81a1913329 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 10:22:25 +0100 Subject: [PATCH 12/28] spec/REGW: introduce REGW chip --- spec/book.typ | 1 + spec/regw.typ | 67 ++++++++++++++++ spec/src/regw.toml | 167 +++++++++++++++++++++++++++++++++++++++ spec/src/signatures.toml | 13 +++ 4 files changed, 248 insertions(+) create mode 100644 spec/regw.typ create mode 100644 spec/src/regw.toml diff --git a/spec/book.typ b/spec/book.typ index bf8b044ec..e0bd602ad 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -21,6 +21,7 @@ ("shift.typ", [SHIFT chip], ), ("branch.typ", [BRANCH chip], ), ("memw.typ", [MEMW chip], ), + ("regw.typ", [REGW chip], ), ("lt.typ", [LT chip], ), ("mul.typ", [MUL chip], ), ("dvrm.typ", [DVRM chip], ), diff --git a/spec/regw.typ b/spec/regw.typ new file mode 100644 index 000000000..3226bc378 --- /dev/null +++ b/spec/regw.typ @@ -0,0 +1,67 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_assumptions, + render_chip_padding_table, +) + +#let config = load_config() +#let chip = load_chip("src/regw.toml", config) + +#show: book-page(chip.name) + +#let reg = raw(chip.name) + +The #reg chip is used to read and write register locations. +It introduces the `old` value and last-accessed timestamps of the registers internally, in order to satisfy the design of the memory argument (@memory). + += Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +#let stackrel(top, bottom) = { + $mat(delim: #none, top; bottom)$ +} + += Assumptions +The following range checks are assumed to be performed/enforced outside of this chip: +#render_chip_assumptions(chip, config) + += Constraints +One of the primary tests this chip performs, is verify that $#`old_timestamp`<#`timestamp`$. +This is achieved by ensuring that adding $#`timestamp_diff` := #`old_timestamp` - #`timestamp`$ to `timestamp` overflows. +This is asserted by means of the following constraints: +#render_constraint_table(chip, config, groups: "sub") + +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(chip, config, groups: "interactions") + +This chip can either just write ($#`μ_write` = 1$), or read&written in the same cycle ($#`μ_read` = 1$). +However, it must be asserted that at most one of these two options is selected: +#render_constraint_table(chip, config, groups: "multiplicities") + +Lastly, this chip contributes the following interactions to the logup: +#render_constraint_table(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(chip, config) + += Notes +- Given that most accesses are to "hot" register (i.e., registers that are accessed often), `timestamp_diff` will rarely be large. + This might allow `timestamp_diff` to be reduced to `Half` in a fast-path version of this chip. + It could even be that `old_timestamp[1]` can be dropped. Things would then be computed as + - `carry[0] = (old_timestamp[0] + timestamp_diff - timestamp[0]) / 2^32` + - `IS_HALF[timestamp_diff-1]` to ensure diff is at least 1 + - `old_timestamp[1] = timestamp[1] - carry[0]` + - `carry[1] = 0` to ensure old_ts < ts + (-4 col) +- Most register accesses both read&write (and not just read). The fast-path chip could assume this to always be the case, allowing the two multiplicities to be merged. (-1 col) \ No newline at end of file diff --git a/spec/src/regw.toml b/spec/src/regw.toml new file mode 100644 index 000000000..658850f4f --- /dev/null +++ b/spec/src/regw.toml @@ -0,0 +1,167 @@ +name = "REGW" + +# Variables + +[[variables.input]] +name = "index" +type = "Byte" +desc = "index 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" +type = "DWordWL" +desc = "timestamp at which this register was last accessed" +pad = 0 + +[[variables.auxiliary]] +name = "timestamp_diff" +type = "DWordHL" +desc = "$#`old_timestamp` - #`timestamp`$" +pad = 0 + +[[variables.virtual]] +name = "carry" +desc = "Carry values used to constrain that $#`old_timestamp`<#`timestamp`$" +type = ["Bit", 2] +def = {idx="i", polys=[ + {iter=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "timestamp", 0], ["idx", ["cast", "timestamp_diff", "DWordWL"], 0]], ["idx", "old_timestamp", 0]]]}, + {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "timestamp", 1], ["idx", ["cast", "timestamp_diff", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", "old_timestamp", 1]]]}, +]} + +[[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_BYTE[index]`" +ref = "regw:a:index" + +[[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 = "sub" + +[[constraints.sub]] +kind = "interaction" +tag = "IS_HALF" +input = [["idx", "timestamp_diff", "i"]] +iter = ["i", 0, 3] +multiplicity = "μ_sum" +ref = "regw:c:range_timestamp_diff" + +[[constraints.sub]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "carry", 0]] +ref = "regw:c:carry" + +[[constraints.sub]] +kind = "arith" +constraint = "$#`carry`_1 = 1$" +poly = ["-", 1, ["idx", "carry", 1]] +ref = "regw:c:no_overflow" + + +[[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, ["cast", ["arr", ["cast", ["+", ["*", 2, "index"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] +iter = ["i", 0, 1] +multiplicity = "μ_sum" +ref = "regw:c:read_old" + +[[constraints.interactions]] +kind = "interaction" +tag = "memory" +input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "index"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] +iter = ["i", 0, 1] +multiplicity = ["-", "μ_sum"] +ref = "regw:c:write_val" + + +[[constraint_groups]] +name = "output" + +[[constraints.output]] +kind = "interaction" +tag = "REG" +input = ["index", "timestamp", "val"] +output = "old" +multiplicity = ["-", "μ_read"] + +[[constraints.output]] +kind = "interaction" +tag = "REG" +input = ["index", "timestamp", "val"] +multiplicity = ["-", "μ_write"] \ No newline at end of file diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 17ecd3933..a7d07ff34 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -69,6 +69,19 @@ tag = "MEMW" kind = "interaction" input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"] +# REG[old; index, value, timestamp] +[[signatures]] +tag = "REG" +kind = "interaction" +input = ["Byte", "DWordWL", "DWordWL"] +output = "DWordWL" + +# REG[index, value, timestamp] +[[signatures]] +tag = "REG" +kind = "interaction" +input = ["Byte", "DWordWL", "DWordWL"] + # LT[lt; lhs, rhs, signed] [[signatures]] tag = "LT" From 1e2cb68388498f7f5ca09d1d9a256abdbef70587 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 13:29:17 +0100 Subject: [PATCH 13/28] spec/MEMW_R: move REG to MEMW_R --- spec/book.typ | 1 - spec/memw.typ | 51 ++++++++++++++++ spec/regw.typ | 67 ---------------------- spec/src/{regw.toml => memw_register.toml} | 24 ++++---- spec/src/signatures.toml | 13 ----- 5 files changed, 63 insertions(+), 93 deletions(-) delete mode 100644 spec/regw.typ rename spec/src/{regw.toml => memw_register.toml} (79%) diff --git a/spec/book.typ b/spec/book.typ index e0bd602ad..bf8b044ec 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -21,7 +21,6 @@ ("shift.typ", [SHIFT chip], ), ("branch.typ", [BRANCH chip], ), ("memw.typ", [MEMW chip], ), - ("regw.typ", [REGW chip], ), ("lt.typ", [LT chip], ), ("mul.typ", [MUL chip], ), ("dvrm.typ", [DVRM chip], ), diff --git a/spec/memw.typ b/spec/memw.typ index f70496aa8..7e0cbbfb2 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -6,6 +6,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, + render_chip_padding_table ) #let config = load_config() @@ -87,6 +88,56 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu #render_chip_assumptions(alignedchip, config) #render_constraint_table(alignedchip, config) += Register fast-path + +#let config = load_config() +#let register_chip = load_chip("src/memw_register.toml", config) +#let reg = raw(register_chip.name) + +Given that i) there are significantly fewer registers than memory addresses, and ii) registers are accessed far more frequently, a fast-path is devised. + +== 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 +One of the primary tests this chip performs, is verify that $#`old_timestamp`<#`timestamp`$. +This is achieved by ensuring that adding $#`timestamp_diff` := #`old_timestamp` - #`timestamp`$ to `timestamp` overflows. +This is asserted by means of the following constraints: +#render_constraint_table(register_chip, config, groups: "sub") + +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 read&written in the same cycle ($#`μ_read` = 1$). +However, 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) + +== Notes +- Given that most accesses are to "hot" register (i.e., registers that are accessed often), `timestamp_diff` will rarely be large. + This might allow `timestamp_diff` to be reduced to `Half` in a fast-path version of this chip. + It could even be that `old_timestamp[1]` can be dropped. Things would then be computed as + - `carry[0] = (old_timestamp[0] + timestamp_diff - timestamp[0]) / 2^32` + - `IS_HALF[timestamp_diff-1]` to ensure diff is at least 1 + - `old_timestamp[1] = timestamp[1] - carry[0]` + - `carry[1] = 0` to ensure old_ts < ts + (-4 col) +- Most register accesses both read&write (and not just read). The fast-path chip could assume this to always be the case, allowing the two multiplicities to be merged. (-1 col) = Future optimization ideas diff --git a/spec/regw.typ b/spec/regw.typ deleted file mode 100644 index 3226bc378..000000000 --- a/spec/regw.typ +++ /dev/null @@ -1,67 +0,0 @@ -#import "/book.typ": book-page -#import "/src.typ": load_config, load_chip -#import "/chip.typ": ( - render_chip_column_table, - total_nr_variables, - total_nr_instantiated_columns, - render_constraint_table, - render_chip_assumptions, - render_chip_padding_table, -) - -#let config = load_config() -#let chip = load_chip("src/regw.toml", config) - -#show: book-page(chip.name) - -#let reg = raw(chip.name) - -The #reg chip is used to read and write register locations. -It introduces the `old` value and last-accessed timestamps of the registers internally, in order to satisfy the design of the memory argument (@memory). - -= Columns -#let nr_variables = total_nr_variables(chip) -#let nr_columns = total_nr_instantiated_columns(chip, config) - -The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: -#render_chip_column_table(chip, config) - -#let stackrel(top, bottom) = { - $mat(delim: #none, top; bottom)$ -} - -= Assumptions -The following range checks are assumed to be performed/enforced outside of this chip: -#render_chip_assumptions(chip, config) - -= Constraints -One of the primary tests this chip performs, is verify that $#`old_timestamp`<#`timestamp`$. -This is achieved by ensuring that adding $#`timestamp_diff` := #`old_timestamp` - #`timestamp`$ to `timestamp` overflows. -This is asserted by means of the following constraints: -#render_constraint_table(chip, config, groups: "sub") - -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(chip, config, groups: "interactions") - -This chip can either just write ($#`μ_write` = 1$), or read&written in the same cycle ($#`μ_read` = 1$). -However, it must be asserted that at most one of these two options is selected: -#render_constraint_table(chip, config, groups: "multiplicities") - -Lastly, this chip contributes the following interactions to the logup: -#render_constraint_table(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(chip, config) - -= Notes -- Given that most accesses are to "hot" register (i.e., registers that are accessed often), `timestamp_diff` will rarely be large. - This might allow `timestamp_diff` to be reduced to `Half` in a fast-path version of this chip. - It could even be that `old_timestamp[1]` can be dropped. Things would then be computed as - - `carry[0] = (old_timestamp[0] + timestamp_diff - timestamp[0]) / 2^32` - - `IS_HALF[timestamp_diff-1]` to ensure diff is at least 1 - - `old_timestamp[1] = timestamp[1] - carry[0]` - - `carry[1] = 0` to ensure old_ts < ts - (-4 col) -- Most register accesses both read&write (and not just read). The fast-path chip could assume this to always be the case, allowing the two multiplicities to be merged. (-1 col) \ No newline at end of file diff --git a/spec/src/regw.toml b/spec/src/memw_register.toml similarity index 79% rename from spec/src/regw.toml rename to spec/src/memw_register.toml index 658850f4f..f98aa2b46 100644 --- a/spec/src/regw.toml +++ b/spec/src/memw_register.toml @@ -1,11 +1,11 @@ -name = "REGW" +name = "MEMW_R" # Variables [[variables.input]] -name = "index" +name = "address" type = "Byte" -desc = "index of the register being accessed" +desc = "address of the register being accessed" pad = 0 [[variables.input]] @@ -70,8 +70,8 @@ pad = 0 # Assumptions [[assumptions]] -desc = "`IS_BYTE[index]`" -ref = "regw:a:index" +desc = "`IS_BYTE[address]`" +ref = "regw:a:address" [[assumptions]] desc = "`IS_WORD[val[i]]`" @@ -136,7 +136,7 @@ name = "interactions" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "index"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] iter = ["i", 0, 1] multiplicity = "μ_sum" ref = "regw:c:read_old" @@ -144,7 +144,7 @@ ref = "regw:c:read_old" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "index"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] iter = ["i", 0, 1] multiplicity = ["-", "μ_sum"] ref = "regw:c:write_val" @@ -155,13 +155,13 @@ name = "output" [[constraints.output]] kind = "interaction" -tag = "REG" -input = ["index", "timestamp", "val"] -output = "old" +tag = "MEMW" +input = [1, ["cast", ["arr", ["cast", "address", "Word"], 0], "DWordWL"], ["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 = "REG" -input = ["index", "timestamp", "val"] +tag = "MEMW" +input = [1, ["cast", ["arr", ["cast", "address", "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] multiplicity = ["-", "μ_write"] \ No newline at end of file diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index a7d07ff34..17ecd3933 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -69,19 +69,6 @@ tag = "MEMW" kind = "interaction" input = ["Bit", "DWordWL", ["BaseField", 8], "DWordWL", "Bit", "Bit", "Bit"] -# REG[old; index, value, timestamp] -[[signatures]] -tag = "REG" -kind = "interaction" -input = ["Byte", "DWordWL", "DWordWL"] -output = "DWordWL" - -# REG[index, value, timestamp] -[[signatures]] -tag = "REG" -kind = "interaction" -input = ["Byte", "DWordWL", "DWordWL"] - # LT[lt; lhs, rhs, signed] [[signatures]] tag = "LT" From e01db15318cc1f97d4711f4175056c11e3180b27 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:21:19 +0100 Subject: [PATCH 14/28] spec/MEMW_R: optimize --- spec/memw.typ | 42 ++++++++++++++++++------------------- spec/src/memw_register.toml | 32 ++++++++++------------------ 2 files changed, 32 insertions(+), 42 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 7e0cbbfb2..ac86c5dff 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -94,7 +94,17 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu #let register_chip = load_chip("src/memw_register.toml", config) #let reg = raw(register_chip.name) -Given that i) there are significantly fewer registers than memory addresses, and ii) registers are accessed far more frequently, a fast-path is devised. +The #reg chip provides a fast-path for accessing registers. +This fast-path leverages that the facts 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 on the second point above, 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`. == Columns #let nr_variables = total_nr_variables(register_chip) @@ -108,16 +118,20 @@ The following range checks are assumed to be performed/enforced outside of this #render_chip_assumptions(register_chip, config) == Constraints -One of the primary tests this chip performs, is verify that $#`old_timestamp`<#`timestamp`$. -This is achieved by ensuring that adding $#`timestamp_diff` := #`old_timestamp` - #`timestamp`$ to `timestamp` overflows. -This is asserted by means of the following constraints: -#render_constraint_table(register_chip, config, groups: "sub") +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 upperlimbs twice, it is instead assumed that +$#`old_timestamp[0]` = #`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 read&written in the same cycle ($#`μ_read` = 1$). -However, it must be asserted that at most one of these two options is selected: +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: @@ -125,22 +139,8 @@ Lastly, this chip contributes the following interactions to the logup: == Padding The table can be padded to the next power of two with the following value assignments: - #render_chip_padding_table(register_chip, config) -== Notes -- Given that most accesses are to "hot" register (i.e., registers that are accessed often), `timestamp_diff` will rarely be large. - This might allow `timestamp_diff` to be reduced to `Half` in a fast-path version of this chip. - It could even be that `old_timestamp[1]` can be dropped. Things would then be computed as - - `carry[0] = (old_timestamp[0] + timestamp_diff - timestamp[0]) / 2^32` - - `IS_HALF[timestamp_diff-1]` to ensure diff is at least 1 - - `old_timestamp[1] = timestamp[1] - carry[0]` - - `carry[1] = 0` to ensure old_ts < ts - (-4 col) -- Most register accesses both read&write (and not just read). The fast-path chip could assume this to always be the case, allowing the two multiplicities to be merged. (-1 col) - = 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. diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index f98aa2b46..9e8903ed0 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -27,25 +27,16 @@ desc = "value of this register at `old_timestamp`." pad = 0 [[variables.auxiliary]] -name = "old_timestamp" -type = "DWordWL" -desc = "timestamp at which this register was last accessed" -pad = 0 - -[[variables.auxiliary]] -name = "timestamp_diff" -type = "DWordHL" -desc = "$#`old_timestamp` - #`timestamp`$" +name = "old_timestamp_lo" +type = "Word" +desc = "the lower limb of `old_timestamp`" pad = 0 [[variables.virtual]] -name = "carry" -desc = "Carry values used to constrain that $#`old_timestamp`<#`timestamp`$" -type = ["Bit", 2] -def = {idx="i", polys=[ - {iter=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "timestamp", 0], ["idx", ["cast", "timestamp_diff", "DWordWL"], 0]], ["idx", "old_timestamp", 0]]]}, - {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "timestamp", 1], ["idx", ["cast", "timestamp_diff", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", "old_timestamp", 1]]]}, -]} +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" @@ -86,15 +77,14 @@ ref = "regw:a:timestamp" # Constraints [[constraint_groups]] -name = "sub" +name = "diff" -[[constraints.sub]] +[[constraints.diff]] kind = "interaction" tag = "IS_HALF" -input = [["idx", "timestamp_diff", "i"]] -iter = ["i", 0, 3] +input = [["-", ["idx", "timestamp", 0], ["idx", "old_timestamp", 0], 1]] multiplicity = "μ_sum" -ref = "regw:c:range_timestamp_diff" +ref = "regw:c:diff" [[constraints.sub]] kind = "template" From 5eaacc25209617719d9ae2e3b245ac66d9287758 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:23:04 +0100 Subject: [PATCH 15/28] spec/MEMW_A: padding --- spec/memw.typ | 4 ++++ spec/src/memw_aligned.toml | 11 +++++++++++ 2 files changed, 15 insertions(+) diff --git a/spec/memw.typ b/spec/memw.typ index ac86c5dff..deaa3d5bb 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -88,6 +88,10 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu #render_chip_assumptions(alignedchip, config) #render_constraint_table(alignedchip, config) +== Padding +The table can be padded to the next power of two with the following value assignments: +#render_chip_padding_table(alignedchip, config) + = Register fast-path #let config = load_config() diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index be6bb1603..757ac4dee 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -6,36 +6,43 @@ name = "MEMW_A" name = "is_register" type = "Bit" desc = "Whether the address represents a register index" +pad = 0 [[variables.input]] name = "base_address" type = "DWordWHH" desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access" +pad = 0 [[variables.input]] name = "value" type = ["BaseField", 8] desc = "The values to store in memory. For regular memory, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" +pad = 0 [[variables.input]] name = "timestamp" type = "DWordWL" desc = "The timestamp at which this memory access is said to occur" +pad = 0 [[variables.input]] name = "write2" type = "Bit" desc = "Whether to write exactly 2 values" +pad = 0 [[variables.input]] name = "write4" type = "Bit" desc = "Whether to write exactly 4 values" +pad = 0 [[variables.input]] name = "write8" type = "Bit" desc = "Whether to write exactly 8 values" +pad = 0 # Output @@ -44,6 +51,7 @@ name = "old" type = ["BaseField", 8] desc = """The old value written at `base_address + i`. See `value` for information about representation. Only the elements corresponding to the `writeN` bits are guaranteed""" +pad = 0 # Auxiliary @@ -51,6 +59,7 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" name = "old_timestamp" type = "DWordWL" desc = "The timestamp at which the address was last accessed" +pad = 0 # Virtual @@ -78,11 +87,13 @@ def = ["+", "μ_read", "μ_write"] 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]] desc = "`IS_HALF[base_address[i]]`" From 7c8927b64d58996419d9fa56b1afc0cad4054630 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:45:13 +0100 Subject: [PATCH 16/28] spec/MEMW_R: touch ups --- spec/memw.typ | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index deaa3d5bb..1832ccf9e 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -99,15 +99,15 @@ The table can be padded to the next power of two with the following value assign #let reg = raw(register_chip.name) The #reg chip provides a fast-path for accessing registers. -This fast-path leverages that the facts that 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 on the second point above, this chip can only be used for register accesses for which +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$ ++ $#`timestamp` mod 2^ > #`old_timestamp`_0$ If either of these rules does not apply to your access, you should fall back to using `MEMW_A`. == Columns From 2a1d8e37b2a56c8a6755a9c88044f0ad90b05a40 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:49:56 +0100 Subject: [PATCH 17/28] spec/MEMW_R: drop superfluous constraints --- spec/src/memw_register.toml | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 9e8903ed0..b4dac453b 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -86,18 +86,6 @@ input = [["-", ["idx", "timestamp", 0], ["idx", "old_timestamp", 0], 1]] multiplicity = "μ_sum" ref = "regw:c:diff" -[[constraints.sub]] -kind = "template" -tag = "IS_BIT" -input = [["idx", "carry", 0]] -ref = "regw:c:carry" - -[[constraints.sub]] -kind = "arith" -constraint = "$#`carry`_1 = 1$" -poly = ["-", 1, ["idx", "carry", 1]] -ref = "regw:c:no_overflow" - [[constraint_groups]] name = "multiplicities" From ed889ff33a117af66b6822dd49087a38ed794164 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:55:04 +0100 Subject: [PATCH 18/28] spec/MEMW_R: minor fixes --- spec/memw.typ | 4 ++-- spec/src/memw_register.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 1832ccf9e..9afac2827 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -107,7 +107,7 @@ to achieve a footprint that is significantly smaller than both #memw and #aligne 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` mod 2^ > #`old_timestamp`_0$ ++ $#`timestamp[0]` > #`old_timestamp[0]`$ If either of these rules does not apply to your access, you should fall back to using `MEMW_A`. == Columns @@ -124,7 +124,7 @@ The following range checks are assumed to be performed/enforced outside of this == 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 upperlimbs twice, it is instead assumed that -$#`old_timestamp[0]` = #`timestamp[1]`$; #aligned can be used for accesses where this is not the case. +$#`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`. diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index b4dac453b..9808df4a0 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -142,4 +142,4 @@ multiplicity = ["-", "μ_read"] kind = "interaction" tag = "MEMW" input = [1, ["cast", ["arr", ["cast", "address", "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] -multiplicity = ["-", "μ_write"] \ No newline at end of file +multiplicity = ["-", "μ_write"] From cc33da8d1e86b528c7a5e3c5e08caa18ac26e3d7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 15:32:44 +0100 Subject: [PATCH 19/28] spec/MEMW_R: fix address mul 2 bug --- spec/src/memw_register.toml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 9808df4a0..3ffd700b1 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -4,7 +4,7 @@ name = "MEMW_R" [[variables.input]] name = "address" -type = "Byte" +type = "Half" desc = "address of the register being accessed" pad = 0 @@ -114,7 +114,7 @@ name = "interactions" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", "address", "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] iter = ["i", 0, 1] multiplicity = "μ_sum" ref = "regw:c:read_old" @@ -122,7 +122,7 @@ ref = "regw:c:read_old" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", "address", "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] iter = ["i", 0, 1] multiplicity = ["-", "μ_sum"] ref = "regw:c:write_val" From 75199d54b4c408679108f8318bb9ddd37bbcd583 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 16:01:47 +0100 Subject: [PATCH 20/28] spec/MEMW: fix multiplicities --- spec/src/memw.toml | 4 ++-- spec/src/memw_aligned.toml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 4905fc5aa..4ae5490c4 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -235,10 +235,10 @@ kind = "interaction" tag = "MEMW" input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] output = "old" -multiplicity = "μ_read" +multiplicity = ["-", "μ_read"] [[constraints.output]] kind = "interaction" tag = "MEMW" input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] -multiplicity = "μ_write" +multiplicity = ["-", "μ_write"] diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index be6bb1603..b808c7a47 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -200,10 +200,10 @@ kind = "interaction" tag = "MEMW" input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] output = "old" -multiplicity = "μ_read" +multiplicity = ["-", "μ_read"] [[constraints.output]] kind = "interaction" tag = "MEMW" input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] -multiplicity = "μ_write" +multiplicity = ["-", "μ_write"] From 55ed2e6ad9b603ac76a3c0fa3df294cdd0cf5f21 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 14:23:04 +0100 Subject: [PATCH 21/28] spec/MEMW_A: padding --- spec/memw.typ | 4 ++++ spec/src/memw_aligned.toml | 11 +++++++++++ 2 files changed, 15 insertions(+) diff --git a/spec/memw.typ b/spec/memw.typ index f70496aa8..ebeeb6074 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -6,6 +6,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, + render_chip_padding_table, ) #let config = load_config() @@ -87,6 +88,9 @@ The #aligned chip only needs #nr_variables variables, expressed through #nr_colu #render_chip_assumptions(alignedchip, config) #render_constraint_table(alignedchip, config) +== Padding +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 diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index b808c7a47..ff43c7bb5 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -6,36 +6,43 @@ name = "MEMW_A" name = "is_register" type = "Bit" desc = "Whether the address represents a register index" +pad = 0 [[variables.input]] name = "base_address" type = "DWordWHH" desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access" +pad = 0 [[variables.input]] name = "value" type = ["BaseField", 8] desc = "The values to store in memory. For regular memory, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" +pad = 0 [[variables.input]] name = "timestamp" type = "DWordWL" desc = "The timestamp at which this memory access is said to occur" +pad = 0 [[variables.input]] name = "write2" type = "Bit" desc = "Whether to write exactly 2 values" +pad = 0 [[variables.input]] name = "write4" type = "Bit" desc = "Whether to write exactly 4 values" +pad = 0 [[variables.input]] name = "write8" type = "Bit" desc = "Whether to write exactly 8 values" +pad = 0 # Output @@ -44,6 +51,7 @@ name = "old" type = ["BaseField", 8] desc = """The old value written at `base_address + i`. See `value` for information about representation. Only the elements corresponding to the `writeN` bits are guaranteed""" +pad = 0 # Auxiliary @@ -51,6 +59,7 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" name = "old_timestamp" type = "DWordWL" desc = "The timestamp at which the address was last accessed" +pad = 0 # Virtual @@ -78,11 +87,13 @@ def = ["+", "μ_read", "μ_write"] 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]] desc = "`IS_HALF[base_address[i]]`" From 0b99118bb3897feed0fc5300e1a01a7d7a9f96da Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 16:17:27 +0100 Subject: [PATCH 22/28] spec/MEMW: padding --- spec/memw.typ | 4 ++++ spec/src/memw.toml | 13 ++++++++++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/spec/memw.typ b/spec/memw.typ index ebeeb6074..b1f95a491 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -65,6 +65,10 @@ to effectuate that part of the memory argument. This chip contributes the following to the lookup argument: #render_constraint_table(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(chip, config) + = Read-size aligned fast path #let alignedchip = load_chip("src/memw_aligned.toml", config) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 4ae5490c4..9ea6e84b3 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -6,36 +6,43 @@ name = "MEMW" name = "is_register" type = "Bit" desc = "Whether the address represents a register index" +pad = 0 [[variables.input]] name = "base_address" type = "DWordWL" desc = "The base address to read from/write to. Gets offset by $[0, 7]$ depending on the size of the access" +pad = 0 [[variables.input]] name = "value" type = ["BaseField", 8] desc = "The values to store in memory. For RAM, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" +pad = 0 [[variables.input]] name = "timestamp" type = "DWordWL" desc = "The timestamp at which this memory access occurs" +pad = 0 [[variables.input]] name = "write2" type = "Bit" desc = "Whether to write exactly 2 values" +pad = 0 [[variables.input]] name = "write4" type = "Bit" desc = "Whether to write exactly 4 values" +pad = 0 [[variables.input]] name = "write8" type = "Bit" desc = "Whether to write exactly 8 values" +pad = 0 # Output @@ -44,6 +51,7 @@ name = "old" type = ["BaseField", 8] desc = """The old value written at `base_address`. See `value` for information about representation. Only the elements corresponding to the `writeN` bits are guaranteed""" +pad = ["arr", 0,0,0,0,0,0,0,0] # Auxiliary @@ -51,11 +59,13 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" name = "carry" type = ["Bit", 7] desc = "Whether `base_address[0] + i + 1` $>= 2^32$" +pad = ["arr", 0,0,0,0,0,0,0] [[variables.auxiliary]] name = "old_timestamp" type = ["DWordWL", 8] desc = "The timestamp at which address `base_address + i` was last accessed" +pad = ["arr", 0,0,0,0,0,0,0,0] # Virtual @@ -92,12 +102,13 @@ def = ["+", "μ_read", "μ_write"] 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]] desc = "`IS_WORD[base_address[i]]`" From c7203e5682aa50be81d43ffc4578ccf1e4521b69 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 16:28:52 +0100 Subject: [PATCH 23/28] spec/MEMW: bit check multiplicities --- spec/src/memw.toml | 10 ++++++++++ spec/src/memw_aligned.toml | 10 ++++++++++ 2 files changed, 20 insertions(+) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 9ea6e84b3..3b7b58622 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -134,6 +134,16 @@ iter = ["i", 0, 1] [[constraint_groups]] name = "consistency" +[[constraints.consistency]] +kind = "template" +tag = "IS_BIT" +input = ["μ_read"] + +[[constraints.consistency]] +kind = "template" +tag = "IS_BIT" +input = ["μ_write"] + [[constraints.consistency]] kind = "template" tag = "IS_BIT" diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index ff43c7bb5..93a636aba 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -128,6 +128,16 @@ tag = "IS_HALF" input = [["+", ["idx", "base_address", 0], "write2", ["*", 3, "write4"], ["*", 7, "write8"]]] multiplicity = "μ_sum" +[[constraints.consistency]] +kind = "template" +tag = "IS_BIT" +input = ["μ_read"] + +[[constraints.consistency]] +kind = "template" +tag = "IS_BIT" +input = ["μ_write"] + [[constraints.consistency]] kind = "template" tag = "IS_BIT" From ea69070c03ad519e40f087e771a57052801110e7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 18:13:47 +0100 Subject: [PATCH 24/28] spec/MEMW_R: apply 2x to address --- spec/memw.typ | 2 ++ spec/src/memw_register.toml | 8 ++++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 674225863..e33a2bc9a 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -114,6 +114,8 @@ Note: as a result of hard optimization, this chip can only be used for register + $#`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) diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 3ffd700b1..788ae7fa7 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -114,7 +114,7 @@ name = "interactions" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", "address", "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] iter = ["i", 0, 1] multiplicity = "μ_sum" ref = "regw:c:read_old" @@ -122,7 +122,7 @@ ref = "regw:c:read_old" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", "address", "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] +input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] iter = ["i", 0, 1] multiplicity = ["-", "μ_sum"] ref = "regw:c:write_val" @@ -134,12 +134,12 @@ name = "output" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = [1, ["cast", ["arr", ["cast", "address", "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +input = [1, ["cast", ["arr", ["cast", ["*", 2, "address"], "Word"], 0], "DWordWL"], ["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, ["cast", ["arr", ["cast", "address", "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +input = [1, ["cast", ["arr", ["cast", ["*", 2, "address"], "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] multiplicity = ["-", "μ_write"] From f5a27aa2614c5d474003a368b0baebd7539be316 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 18:17:32 +0100 Subject: [PATCH 25/28] spec/MEMW_R: remove superfluous casts --- spec/src/memw_register.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 788ae7fa7..d2054f5a3 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -114,7 +114,7 @@ name = "interactions" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "old_timestamp", ["idx", "old", "i"]] +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" @@ -122,7 +122,7 @@ ref = "regw:c:read_old" [[constraints.interactions]] kind = "interaction" tag = "memory" -input = [1, ["cast", ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "DWordWL"], "timestamp", ["idx", "val", "i"]] +input = [1, ["arr", ["cast", ["+", ["*", 2, "address"], "i"], "Word"], 0], "timestamp", ["idx", "val", "i"]] iter = ["i", 0, 1] multiplicity = ["-", "μ_sum"] ref = "regw:c:write_val" @@ -134,12 +134,12 @@ name = "output" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = [1, ["cast", ["arr", ["cast", ["*", 2, "address"], "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +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, ["cast", ["arr", ["cast", ["*", 2, "address"], "Word"], 0], "DWordWL"], ["arr", ["idx", "val", 0], ["idx", "val", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] +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"] From 3750f4077940ed3e5c2904144174404e1f0e344a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 18:19:43 +0100 Subject: [PATCH 26/28] spec/MEMW_R: list future optimization --- spec/memw.typ | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/memw.typ b/spec/memw.typ index e33a2bc9a..1f9395166 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -154,3 +154,4 @@ The table can be padded to the next power of two with the following value assign = Future optimization ideas - `MEMB` chip that does a one-byte write to remove old_timestamp from here (uncertain tradeoffs) - 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 From c9ed517bb6c96aa48cabfb3ea6d170e9a40b0c73 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 23 Mar 2026 18:20:20 +0100 Subject: [PATCH 27/28] spec/MEMW_R: fix typo --- spec/memw.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/memw.typ b/spec/memw.typ index 1f9395166..1c7a1e6e5 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -129,7 +129,7 @@ The following range checks are assumed to be performed/enforced outside of this == 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 upperlimbs twice, it is instead assumed that +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$. From 42b6d189608524ddad28ab68c9102b9c07b9b5aa Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 24 Mar 2026 11:32:10 +0100 Subject: [PATCH 28/28] spec/MEMW_R: fix address --- spec/src/memw_register.toml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index d2054f5a3..3e7cdcf28 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -4,7 +4,7 @@ name = "MEMW_R" [[variables.input]] name = "address" -type = "Half" +type = "Byte" desc = "address of the register being accessed" pad = 0 @@ -60,10 +60,6 @@ pad = 0 # Assumptions -[[assumptions]] -desc = "`IS_BYTE[address]`" -ref = "regw:a:address" - [[assumptions]] desc = "`IS_WORD[val[i]]`" iter = ["i", 0, 1]