From f38c1c7a70c04a650335509691836a7639920445 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 17 Mar 2026 09:26:35 +0100 Subject: [PATCH 01/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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,