diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index 1c1f32095..f4ae00a23 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -34,3 +34,6 @@ Negative numbers (represented as 2s complement 64-bit numbers), are used for our / -2: `KECCAK` (@keccak) / -11: `ECSM`/`secp256k1` (@ecsm) / -12: `ECSM`/`secp256r1` (@ecsm) +/ -20: `FEXT_LOAD` (@fext) +/ -21: `FEXT_FMA` (@fext) +/ -22: `FEXT_ZERO` (@fext) diff --git a/spec/book.typ b/spec/book.typ index e8eb1855c..052f134bd 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -53,6 +53,7 @@ ("sha256.typ", [`SHA256` accelerator], ), ("keccak.typ", [`KECCAK` accelerator], ), ("ecsm.typ", [`ECSM` accelerator], ), + ("fext.typ", [Extension field accelerator], ), )), ("MATHEMATICS", ( ("limbs_and_carries.typ", [On limb decomposition and carries], ), diff --git a/spec/fext.typ b/spec/fext.typ new file mode 100644 index 000000000..95f0ab4f5 --- /dev/null +++ b/spec/fext.typ @@ -0,0 +1,106 @@ +#import "/book.typ": book-page, aside +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_variable_table, + total_nr_variables, + total_nr_instantiated_columns, + compute_nr_interactions, + render_constraint_table, + render_chip_assumptions, + render_chip_padding_table, +) + +#show: book-page("fext.typ") + +#let config = load_config() +#let loadchip = load_chip("src/fext_load.toml", config) +#let load = raw(loadchip.name) +#let fmachip = load_chip("src/fext_fma.toml", config) +#let fma = raw(fmachip.name) +#let zerochip = load_chip("src/fext_zero.toml", config) +#let zero = raw(zerochip.name) + +We introduce a set of chips for faster processing of numbers mod the native goldilocks prime, +or a degree three extension field thereof. +Our approach is to offer an arithmetic black box (ABB), consisting of the #fma and #zero chips, +that operates on a separate memory domain, and the #load chip to bridge the gap +from normal byte-addressed RAM memory to this separate field-storage. +Each 64 bit value is a possibly valid address within the ABB, providing a handle for a single extension field element. +As noted in @memory, we reserve the domain separator values $3$, $4$ and $5$ for field-storage, +such that domain $3 + i$ stores the coefficient for the $X^i$ term of an extension field element. +For global initialization and finalization of the field-storage, we recommend using the same +constant-zero `PAGE` chip as described in @streaming, emitting `GLOBAL_MEM` interactions for domains +$3$, $4$, and $5$. +As an optimization, these three `PAGE` chips could be merge into a single one emitting all three domains, +avoiding the cost of having to commit to the columns multiple times. + += The #load chip +#let nr_variables = total_nr_variables(loadchip) +#let nr_columns = total_nr_instantiated_columns(loadchip, config) +#let nr_interactions = compute_nr_interactions(loadchip) + +We use the #load chip to load the three composing coefficients from registers A1-A3 (in little-endian), +verify that all of them are in the correct range for a field element, +and then write them as field elements into field-storage. +We do this using #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. + +== Variables + +#render_chip_variable_table(loadchip, config) + +== Constraints + +#render_constraint_table(loadchip, config) + +== Padding + +#render_chip_padding_table(loadchip, config) + += The #fma chip +#let nr_variables = total_nr_variables(fmachip) +#let nr_columns = total_nr_instantiated_columns(fmachip, config) +#let nr_interactions = compute_nr_interactions(fmachip) + +To compute a fused multiply-add (FMA) operation `output = a * b + c`, we first load +everything from memory, passing the input (ABB) addresses in A0-A2 and the output address in A3. +Then we constrain the extension field operation, and write back to (ABB) memory. + +The extension field is expressed through three constant columns, $alpha$, $beta$ and $gamma$, +such that the defining polynomial is $X^3 - alpha X^2 - beta X - gamma = 0$, or alternatively, +$X^3 = alpha X^2 + beta X + gamma$. + +== Variables + +We express this chip using #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. + +#render_chip_variable_table(fmachip, config) + +== Constraints + +#render_constraint_table(fmachip, config) + +== Padding + +#render_chip_padding_table(fmachip, config) + += The #zero chip +#let nr_variables = total_nr_variables(zerochip) +#let nr_columns = total_nr_instantiated_columns(zerochip, config) +#let nr_interactions = compute_nr_interactions(zerochip) + +This chip asserts that a field extension element in the ABB, passed in the `A0` register, is zero. +It uses #nr_variables variables spanning #nr_columns columns and #nr_interactions interactions. + +== Variables + +#render_chip_variable_table(zerochip, config) + +== Constraints + +Read the field element address from the `A0` register, and then assert that the field memory reads a zero. + +#render_constraint_table(zerochip, config) + +== Padding + +#render_chip_padding_table(zerochip, config) diff --git a/spec/memory.typ b/spec/memory.typ index bdd299b4b..b3bc8c092 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -25,11 +25,14 @@ and are therefore handled simultaneously. While RAM is byte addressed, we do choose to store registers as a `DWordWL` over two word addresses. ] In particular, our memory addressing scheme will consist of two parts: a domain separator, and an address within the domain. -For specific domains and domain separators, we use the following assignment. +For specific domains and domain separators, we use the following assignment, where we indicate +whether or not each domain should be "paged". +For information on paging, refer to @memory:s:init_fini and @streaming:chip:page. -/ RAM memory: $0$ -/ Registers: $1$ -/ Committed values: $2$ +/ RAM memory: $0$, paged +/ Registers: $1$, unpaged +/ Committed values: $2$, unpaged +/ (Extension) field values: $3$, $4$, $5$, paged On a high level, we ensure memory consistency by an interacting system of reads and writes to a lookup argument, combined with an initialization and finalization scheme. @@ -129,7 +132,7 @@ The `CPU` merely passes in the current timestamp, while `MEMW` can recall the pr ] ] -= Initialization and Finalization += Initialization and Finalization Because the LogUp argument handling token consumption and emission needs to be fully balanced --- every token emitted should be consumed, and vice versa --- diff --git a/spec/memw.typ b/spec/memw.typ index 43c0d4e20..5d64e0f9d 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -39,7 +39,7 @@ provide these below. #render_constraint_table(chip, config, groups: "assumptions") -Our assumptions do not explicitly cover any range checks for the `is_register` and `value` columns, +Our assumptions do not explicitly cover any range checks for the `value` column, as these are not necessary for the correctness of this chip in isolation. 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. diff --git a/spec/src/fext_fma.toml b/spec/src/fext_fma.toml new file mode 100644 index 000000000..1adb99eb0 --- /dev/null +++ b/spec/src/fext_fma.toml @@ -0,0 +1,144 @@ +name = "FEXT_FMA" +code = "FMA" + +[[variables.input]] +name = "input_addrs" +type = ["DWordWL", 3] +desc = "The addresses of `values`" +pad = 0 + +[[variables.input]] +name = "output_addr" +type = "DWordWL" +desc = "The address of `output`" +pad = 0 + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.auxiliary]] +name = "values" +type = [["BaseField", 3], 3] +desc = "The value to operate on: `a`, `b`, `c` in order to compute `a * b + c`" +pad = 0 + +[[variables.output]] +name = "output" +type = ["BaseField", 3] +desc = "The output value" +pad = 0 + +[[variables.constant]] +name = "α" +type = "BaseField" +desc = "The $#`X`^2$ coefficient of the defining polynomial" + +[[variables.constant]] +name = "β" +type = "BaseField" +desc = "The $#`X`^1$ coefficient of the defining polynomial" + +[[variables.constant]] +name = "γ" +type = "BaseField" +desc = "The $#`X`^0$ coefficient of the defining polynomial" + +[[variables.virtual]] +name = "a" +type = ["BaseField", 3] +def = ["idx", "values", 0] +desc = "" + +[[variables.virtual]] +name = "b" +type = ["BaseField", 3] +def = ["idx", "values", 1] +desc = "" + +[[variables.virtual]] +name = "c" +type = ["BaseField", 3] +def = ["idx", "values", 2] +desc = "" + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "REG" +input = [["+", 10, "i"], ["idx", "input_addrs", "i"], "timestamp"] +output = ["idx", "input_addrs", "i"] +iter = ["i", 0, 2] +cond = "μ" + +[[constraints.all]] +kind = "template" +tag = "REG" +input = [13, "output_addr", "timestamp"] +output = "output_addr" +cond = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "d"], ["idx", "input_addrs", "i"], ["arr", ["idx", ["idx", "values", "i"], "d"], 0, 0, 0, 0, 0, 0, 0], ["+", "timestamp", "i"], 0, 0, 0] +output = ["arr", ["idx", ["idx", "values", "i"], "d"], 0, 0, 0, 0, 0, 0, 0] +iters = [["d", 0, 2], ["i", 0, 2]] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "d"], "output_addr", ["arr", ["idx", "output", "d"], 0, 0, 0, 0, 0, 0, 0], ["+", "timestamp", 3], 0, 0, 0] +multiplicity = "μ" +iter = ["d", 0, 2] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[0]` = a_0 b_0 + gamma (a_1 b_2 + a_2 b_1 + alpha dot a_2 b_2) + c_0$" +poly = ["-", ["idx", "output", 0], + ["*", ["idx", "a", 0], ["idx", "b", 0]], + ["*", "γ", ["+", + ["*", ["idx", "a", 1], ["idx", "b", 2]], + ["*", ["idx", "a", 2], ["idx", "b", 1]], + ["*", "α", ["idx", "a", 2], ["idx", "b", 2]]]], + ["idx", "c", 0]] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[1]` = a_0 b_1 + a_1 b_0 + beta (a_1 b_2 + a_2 b_1) + (alpha beta + gamma) a_2 b_2 + c_1$" +poly = ["-", ["idx", "output", 1], + ["*", ["idx", "a", 0], ["idx", "b", 1]], + ["*", ["idx", "a", 1], ["idx", "b", 0]], + ["*", "β", ["idx", "a", 1], ["idx", "b", 2]], + ["*", "β", ["idx", "a", 2], ["idx", "b", 1]], + ["*", ["+", ["*", "α", "β"], "γ"], ["idx", "a", 2], ["idx", "b", 2]], + ["idx", "c", 1]] + +[[constraints.all]] +kind = "arith" +constraint = "$#`output[2]` = a_0 b_2 + a_1 b_1 + a_2 b_0 + alpha (a_1 b_2 + a_2 b_1) + (alpha^2 + beta) a_2 b_2 + c_2$" +poly = ["-", ["idx", "output", 2], + ["*", ["idx", "a", 0], ["idx", "b", 2]], + ["*", ["idx", "a", 1], ["idx", "b", 1]], + ["*", ["idx", "a", 2], ["idx", "b", 0]], + ["*", "α", ["idx", "a", 1], ["idx", "b", 2]], + ["*", "α", ["idx", "a", 2], ["idx", "b", 1]], + ["*", ["+", ["*", "α", "α"], "β"], ["idx", "a", 2], ["idx", "b", 2]], + ["idx", "c", 2]] + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 21], ["-", ["^", 2, 32], 1]]] +multiplicity = ["-", "μ"] diff --git a/spec/src/fext_load.toml b/spec/src/fext_load.toml new file mode 100644 index 000000000..5b00c44a3 --- /dev/null +++ b/spec/src/fext_load.toml @@ -0,0 +1,66 @@ +name = "FEXT_LOAD" +code = "FXL" + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.input]] +name = "addr" +type = "DWordWL" +desc = "The address at which to store the field element" +pad = 0 + +[[variables.input]] +name = "coeffs" +type = ["DWordWL", 3] +desc = "The extension field element coefficients, in native form" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "REG" +input = [10, "addr", "timestamp"] +output = "addr" +cond = "μ" + +[[constraints.all]] +kind = "template" +tag = "REG" +input = [["+", 11, "i"], ["idx", "coeffs", "i"], "timestamp"] +output = ["idx", "coeffs", "i"] +cond = "μ" +iter = ["i", 0, 2] + +[[constraints.all]] +kind = "interaction" +tag = "ALU" +input = [["idx", "coeffs", "i"], ["arr", 1, ["-", ["^", 2, 32], 1]], ["opsel", "LT"]] +output = ["cast", 1, "DWordWL"] +iter = ["i", 0, 2] +multiplicity = "μ" + +# This can either happen directly, or we introduce another dedicated MEMW accelerator? +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "i"], "addr", ["arr", ["+", ["*", ["^", 2, 32], ["idx", ["idx", "coeffs", "i"], 1]], ["idx", ["idx", "coeffs", "i"], 0]], 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0] +iter = ["i", 0, 2] +multiplicity = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 20], ["-", ["^", 2, 32], 1]]] +multiplicity = ["-", "μ"] diff --git a/spec/src/fext_zero.toml b/spec/src/fext_zero.toml new file mode 100644 index 000000000..c4f29ad53 --- /dev/null +++ b/spec/src/fext_zero.toml @@ -0,0 +1,45 @@ +name = "FEXT_ZERO" +code = "FXZ" + +[[variables.input]] +name = "timestamp" +type = "Word" +desc = "The timestamp" +pad = 0 + +[[variables.input]] +name = "addr" +type = "DWordWL" +desc = "The address to assert equal to zero" +pad = 0 + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" +pad = 0 + +[[constraint_groups]] +name = "all" + +[[constraints.all]] +kind = "template" +tag = "REG" +input = [10, "addr", "timestamp"] +output = "addr" +cond = "μ" + +[[constraints.all]] +kind = "interaction" +tag = "MEMW" +input = [["+", 3, "d"], "addr", ["cast", 0, ["BaseField", 8]], "timestamp", 0, 0, 0] +output = ["cast", 0, ["BaseField", 8]] +multiplicity = "μ" +iter = ["d", 0, 2] + +[[constraints.all]] +kind = "interaction" +tag = "ECALL" +input = ["timestamp", ["arr", ["-", ["^", 2, 32], 22], ["-", ["^", 2, 32], 1]]] +multiplicity = ["-", "μ"] + diff --git a/spec/src/memw.toml b/spec/src/memw.toml index eb1ee42b2..3f9011d44 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -4,9 +4,9 @@ code = "MMW" # Input [[variables.input]] -name = "is_register" -type = "Bit" -desc = "Whether the address represents a register index" +name = "domain" +type = "BaseField" +desc = "The memory domain" pad = 0 [[variables.input]] @@ -218,52 +218,52 @@ name = "memory" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", "base_address", ["idx", "old_timestamp", 0], ["idx", "old", 0]] +input = ["domain", "base_address", ["idx", "old_timestamp", 0], ["idx", "old", 0]] multiplicity = "μ_sum" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", "base_address", "timestamp", ["idx", "value", 0]] +input = ["domain", "base_address", "timestamp", ["idx", "value", 0]] multiplicity = ["-", "μ_sum"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]] +input = ["domain", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]] multiplicity = "w2" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]] +input = ["domain", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]] multiplicity = ["-", "w2"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] +input = ["domain", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] multiplicity = "w4" iter = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] +input = ["domain", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "w4"] iter = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] +input = ["domain", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] multiplicity = "write8" iter = ["i", 4, 7] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] +input = ["domain", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "write8"] iter = ["i", 4, 7] @@ -274,12 +274,12 @@ name = "output" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] +input = ["domain", "base_address", "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 = ["domain", "base_address", "value", "timestamp", "write2", "write4", "write8"] multiplicity = ["-", "μ_write"] diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 7838b0b06..6573e7bdc 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -4,9 +4,9 @@ code = "MWA" # Input [[variables.input]] -name = "is_register" -type = "Bit" -desc = "Whether the address represents a register index" +name = "domain" +type = "BaseField" +desc = "The memory domain" pad = 0 [[variables.input]] @@ -183,52 +183,52 @@ name = "memory" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["cast", "base_address", "DWordWL"], "old_timestamp", ["idx", "old", 0]] +input = ["domain", ["cast", "base_address", "DWordWL"], "old_timestamp", ["idx", "old", 0]] multiplicity = "μ_sum" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["cast", "base_address", "DWordWL"], "timestamp", ["idx", "value", 0]] +input = ["domain", ["cast", "base_address", "DWordWL"], "timestamp", ["idx", "value", 0]] multiplicity = ["-", "μ_sum"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "old_timestamp", ["idx", "old", 1]] +input = ["domain", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "old_timestamp", ["idx", "old", 1]] multiplicity = "w2" [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "timestamp", ["idx", "value", 1]] +input = ["domain", ["+", ["cast", "base_address", "DWordWL"], ["cast", 1, "DWordWL"]], "timestamp", ["idx", "value", 1]] multiplicity = ["-", "w2"] [[constraints.memory]] kind = "interaction" tag = "memory" -input = ["is_register", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] +input = ["domain", ["+", ["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", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] +input = ["domain", ["+", ["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", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "old_timestamp", ["idx", "old", "i"]] +input = ["domain", ["+", ["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", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] +input = ["domain", ["+", ["cast", "base_address", "DWordWL"], ["cast", "i", "DWordWL"]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "write8"] iter = ["i", 4, 7] @@ -239,12 +239,12 @@ name = "output" [[constraints.output]] kind = "interaction" tag = "MEMW" -input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] +input = ["domain", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] output = "old" multiplicity = ["-", "μ_read"] [[constraints.output]] kind = "interaction" tag = "MEMW" -input = ["is_register", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] +input = ["domain", ["cast", "base_address", "DWordWL"], "value", "timestamp", "write2", "write4", "write8"] multiplicity = ["-", "μ_write"] diff --git a/spec/src/page.toml b/spec/src/page.toml index e12d89d82..b308a05a5 100644 --- a/spec/src/page.toml +++ b/spec/src/page.toml @@ -7,6 +7,12 @@ name = "page" type = "DWordWL" desc = "Constant column containing the page base address; should be integrated into the constraints directly" +[[variables.constant]] +name = "domain" +type = "Byte" +desc = "The memory domain to provide a page for" + + [[variables.input]] name = "offset" type = "RowIndex" @@ -35,7 +41,6 @@ type = "DWordWL" desc = "Adding `offset` to the page base address `page`. `page` is a constant with respect to a single instance of this table." def = ["+", "page", ["*", "offset", ["cast", 1, "DWordWL"]]] - [[constraint_groups]] name = "all" @@ -47,11 +52,11 @@ input = ["init"] [[constraints.all]] kind = "interaction" tag = "GLOBAL_MEM" -input = [0, "address", 0, "init"] +input = ["domain", "address", 0, "init"] multiplicity = -1 [[constraints.all]] kind = "interaction" tag = "GLOBAL_MEM" -input = [0, "address", "fini_epoch", "fini"] +input = ["domain", "address", "fini_epoch", "fini"] multiplicity = 1 diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index f02ecd163..bdc85f9bf 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -77,11 +77,11 @@ kind = "interaction" input = ["DWordWL", "DWordWL", "DWordWL", "Bit"] output = "DWordWL" -# MEMW[old; is_register, base_address, value, timestamp, write2, write4, write8] +# MEMW[old; domain, base_address, value, timestamp, write2, write4, write8] [[signatures]] tag = "MEMW" kind = "interaction" -input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] +input = ["BaseField", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] output = ["BaseField", 8] # REG[old; base_address, value, timestamp] @@ -92,11 +92,11 @@ input = ["Byte", "DWordWL", "Word"] output = "DWordWL" cond = "BaseField" -# MEMW[is_register, base_address, value, timestamp, write2, write4, write8] +# MEMW[domain, base_address, value, timestamp, write2, write4, write8] [[signatures]] tag = "MEMW" kind = "interaction" -input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] +input = ["BaseField", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] # REG[base_address, value, timestamp] [[signatures]] diff --git a/spec/streaming.typ b/spec/streaming.typ index ef6bd2541..9f435bd56 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -113,7 +113,7 @@ Even though they are not touched by the current epoch, the #l2g chips claims the and simply has finalization clean up the spurious initialization, by setting `fini_value = init_value` and `fini_timestamp = 0`. -= #page chip += #page chip We resume here the description of memory initialization and finalization from @memory, as it applies after integration of the epoch system described above. @@ -121,7 +121,10 @@ Concretely, each page gets an associated `PAGE` table, consisting of #total_nr_v over #total_nr_instantiated_columns(pagechip, config) columns. For each such table, the `page` variable is instantiated as the constant base address of the page. The `offset` column is preprocessed, which helps the verifier ensure that each page has a single fixed size, -but the verifier should still check that no pages overlap and all `page` values are page-aligned. +but the verifier should still check that no pages overlap (per domain) and all `page` values are page-aligned. +The domain variable is instantiated with the specific memory domain (see @memory) for which to instantiate a page, +if the domain is paged. +For unpaged domains, the verifier must ensure no #page chips are present. Observe that this table deals with boundaries on the RAM memory. Registers can still be initialized and finalized in the global memory directly by the verifier, diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index f3e5b58b6..d8e47c680 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -811,7 +811,7 @@ class Assumption: iters: list[Iter] def __init__(self, config: Config, data: dict): - assert_no_unexpected(data, set(self.__annotations__.keys()) | {"iter", "iters", "ref"}) + assert_no_unexpected(data, set(type(self).__annotations__.keys()) | {"iter", "iters", "ref"}) self.desc = data["desc"] self.iters = iters_of(data, config) @@ -824,7 +824,7 @@ class ArithConstraint: iters: list[Iter] def __init__(self, config: Config, data: dict): - assert_no_unexpected(data, set(self.__annotations__.keys()) | {"kind", "ref", "iter", "iters"}) + assert_no_unexpected(data, set(type(self).__annotations__.keys()) | {"kind", "ref", "iter", "iters"}) assert data["kind"] == "arith" self.constraint = data["constraint"] reporter.asserts(