Spec/memw update

spec/memw.typ

@@ -33,44 +33,45 @@ 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 + 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, 
+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.
 
 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
 
 #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.

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/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 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"
@@ -48,14 +48,14 @@ 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$"
+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
 
@@ -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]]

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/write from/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"
-
-[[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"
+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,14 +85,11 @@ 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]`"
+desc = "`IS_HALF[base_address[i]]`"
+iter = ["i", 0, 1]
 
 [[assumptions]]
-desc = "`IS_BYTE[base_address_low[i]]`"
-iter = ["i", 0, 1]
+desc = "`IS_WORD[base_address[2]]`"
 
 [[assumptions]]
 desc = "`IS_BIT<write2>`"
@@ -134,9 +113,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_HALF"
+input = [["+", ["idx", "base_address", 0], "write2", ["*", 3, "write4"], ["*", 7, "write8"]]]
 multiplicity = "μ_sum"
 
 [[constraints.consistency]]
@@ -163,52 +141,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]
 
@@ -220,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"