diff --git a/spec/memw.typ b/spec/memw.typ index 57907e26c..f70496aa8 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 + 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. @@ -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 @@ -68,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. diff --git a/spec/src/memw.toml b/spec/src/memw.toml index c9519e115..4905fc5aa 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/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]] diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 8df912111..be6bb1603 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/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`" @@ -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"