diff --git a/spec/memw.typ b/spec/memw.typ index f70496aa8..b1f95a491 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() @@ -64,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) @@ -87,6 +92,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.toml b/spec/src/memw.toml index 4905fc5aa..1cc0dd3c2 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 = 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 = 0 [[variables.auxiliary]] name = "old_timestamp" type = ["DWordWL", 8] desc = "The timestamp at which address `base_address + i` was last accessed" +pad = 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]]`" @@ -123,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" @@ -235,10 +256,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..93a636aba 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]]`" @@ -117,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" @@ -200,10 +221,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"]