From f38c1c7a70c04a650335509691836a7639920445 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 09:26:35 +0100
Subject: [PATCH 01/16] 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 <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 09:28:18 +0100
Subject: [PATCH 02/16] 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 <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 09:30:40 +0100
Subject: [PATCH 03/16] 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 <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 09:31:00 +0100
Subject: [PATCH 04/16] 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 <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 10:07:57 +0100
Subject: [PATCH 05/16] 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 <erik.takke@3milabs.tech>
Date: Tue, 17 Mar 2026 10:15:14 +0100
Subject: [PATCH 06/16] 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/16] Apply suggestions from code review

Co-authored-by: Robin Jadoul <robin.jadoul@gmail.com>
---
 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<write2>`"
 
@@ -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 <erik.takke@3milabs.tech>
Date: Wed, 18 Mar 2026 10:38:36 +0100
Subject: [PATCH 08/16] 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 <erik.takke@3milabs.tech>
Date: Wed, 18 Mar 2026 10:47:41 +0100
Subject: [PATCH 09/16] 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 <erik.takke@3milabs.tech>
Date: Wed, 18 Mar 2026 10:55:32 +0100
Subject: [PATCH 10/16] 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 <erik.takke@3milabs.tech>
Date: Wed, 18 Mar 2026 11:04:48 +0100
Subject: [PATCH 11/16] 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 75199d54b4c408679108f8318bb9ddd37bbcd583 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 23 Mar 2026 16:01:47 +0100
Subject: [PATCH 12/16] 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 <erik.takke@3milabs.tech>
Date: Mon, 23 Mar 2026 14:23:04 +0100
Subject: [PATCH 13/16] 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 <erik.takke@3milabs.tech>
Date: Mon, 23 Mar 2026 16:17:27 +0100
Subject: [PATCH 14/16] 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 <erik.takke@3milabs.tech>
Date: Mon, 23 Mar 2026 16:28:52 +0100
Subject: [PATCH 15/16] 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 e7d9e01cd99ca05bb752ac0a6a8b204989c6ee3b Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Mon, 23 Mar 2026 17:30:40 +0100
Subject: [PATCH 16/16] spec/MEMW: simplify padding

---
 spec/src/memw.toml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/spec/src/memw.toml b/spec/src/memw.toml
index af38c4d90..1cc0dd3c2 100644
--- a/spec/src/memw.toml
+++ b/spec/src/memw.toml
@@ -51,7 +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]
+pad = 0
 
 # Auxiliary
 
@@ -59,13 +59,13 @@ pad = ["arr",0,0,0,0,0,0,0,0]
 name = "carry"
 type = ["Bit", 7]
 desc = "Whether `base_address[0] + i + 1` $>= 2^32$"
-pad = ["arr",0,0,0,0,0,0,0]
+pad = 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]
+pad = 0
 
 # Virtual