diff --git a/spec/branch.typ b/spec/branch.typ index d01e9fa03..a18c252b7 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -6,6 +6,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, + render_chip_padding_table, ) #let config = load_config() @@ -36,3 +37,8 @@ The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed impli 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) diff --git a/spec/chip.typ b/spec/chip.typ index 84a575c92..ab709c404 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,6 +24,32 @@ .sum() } +#let render_chip_padding_table(chip, config) = { + // Whether `var` is a preprocessed variable. + let is_preprocessed(var) = { + config.variables.types + .filter(t => t.label == var.type) + .all(t => t.at("preprocessed", default: false)) + } + + let instantiated_vars = config.variables.categories.instantiated.map(c => chip.variables.at(c)).flatten() + + show figure: set block(breakable: true) + figure(table( + columns: (auto, auto, auto), + inset: 6pt, + align: (right + top, center + top, left + top), + stroke: none, + table.header([*Column*], [], [*Padding value*]), + table.hline(stroke: stroke(thickness: 2pt)), + ..for var in instantiated_vars { + if not is_preprocessed(var) { + ([#raw(var.name)], [$:=$], [#expr_to_math(var.pad)],) + } + }, + ), caption: [Overview of padding values for #chip.name chip.]) +} + /// Generates a table listing `chip`'s columns. #let render_chip_column_table(chip, config) = { diff --git a/spec/lt.typ b/spec/lt.typ index ff3b6dae3..3b57a62e3 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -3,9 +3,10 @@ #import "/chip.typ": ( render_chip_assumptions, render_chip_column_table, - total_nr_variables, - total_nr_instantiated_columns, + render_chip_padding_table, render_constraint_table, + total_nr_instantiated_columns, + total_nr_variables, ) #let config = load_config() @@ -77,3 +78,9 @@ And then we constrain the subtraction. The 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) diff --git a/spec/mul.typ b/spec/mul.typ index 92fafe26b..1892994f0 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -6,6 +6,7 @@ total_nr_instantiated_columns, render_constraint_table, render_chip_assumptions, + render_chip_padding_table, ) #let config = load_config() @@ -91,4 +92,10 @@ We constrain `lhs_is_negative` and `rhs_is_negative` according to their definiti === Lookup The #mul chip contributes the following to the lookup: -#render_constraint_table(chip, config, groups: "lookup") \ No newline at end of file +#render_constraint_table(chip, config, groups: "lookup") + +== Padding + +The table can be padded to the next power of two with the following value assignments: + +#render_chip_padding_table(chip, config) diff --git a/spec/shift.typ b/spec/shift.typ index 3555d64e4..70aebc97c 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -6,6 +6,7 @@ total_nr_instantiated_columns, render_constraint_table, render_chip_assumptions, + render_chip_padding_table, ) #let config = load_config() @@ -173,3 +174,9 @@ As such, there is no problem with it being unconstrained in this case. === Lookups This chip adds the following interaction to the lookup. #render_constraint_table(chip, config, groups: "lookups") + +== Padding + +The table can be padded to the next power of two with the following value assignments: + +#render_chip_padding_table(chip, config) diff --git a/spec/src/branch.toml b/spec/src/branch.toml index b93639602..d6620dcfd 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -7,21 +7,25 @@ name = "BRANCH" name = "pc" type = "DWordWL" desc = "The current pc, used as base address when `!JALR`" +pad = 0 [[variables.input]] name = "offset" type = "Word" desc = "The offset from the base address to jump to" +pad = 0 [[variables.input]] name = "register" type = "DWordWL" desc = "The base address to use when `JALR`" +pad = 0 [[variables.input]] name = "JALR" type = "Bit" desc = "Selects between `pc` and `register` as base address, needed for the `JALR` instruction" +pad = 0 # Output @@ -30,11 +34,13 @@ desc = "Selects between `pc` and `register` as base address, needed for the `JAL name = "next_pc_high" type = ["Half", 3] desc = "The upper part of the next pc" +pad = 0 # TODO(#128): improve handling for arrays [[variables.output]] name = "next_pc_low" type = ["Byte", 2] desc = "The lower part of the next pc" +pad = 0 # Auxiliary @@ -43,6 +49,7 @@ desc = "The lower part of the next pc" name = "unmasked_low_byte" type = "Byte" desc = "The low byte of the next pc, before masking the LSB. Used to constraint the raw addition." +pad = 0 # Virtual @@ -72,6 +79,7 @@ def = {idx = "i", polys = [ name = "μ" type = "Bit" desc = "" +pad = 0 [[assumptions]] diff --git a/spec/src/config.toml b/spec/src/config.toml index 389e4b16a..68f1683de 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -125,6 +125,7 @@ desc = """\ label = "Timestamp" subtypes = ["DWordWL"] desc = "A preprocessed column holding timestamps as `DWordWL`. Row `i` of the column contains the value $2^2 dot (i + 1)$. Used in the CPU chip, see there for more details about the magic number." +preprocessed = true [variables.categories] all = ["input", "output", "auxiliary", "virtual", "multiplicity", "condition"] diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 1a441c2b3..0ee06abc9 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -7,16 +7,19 @@ name = "LT" name = "lhs" type = "DWordHHW" desc = "The left operand" +pad = 0 [[variables.input]] name = "rhs" type = "DWordHHW" desc = "The right operand" +pad = 0 [[variables.input]] name = "signed" type = "Bit" desc = "whether to interpret `lhs` and `rhs` as signed integers (1) or not (0)" +pad = 0 # Output @@ -24,6 +27,7 @@ desc = "whether to interpret `lhs` and `rhs` as signed integers (1) or not (0)" name = "lt" type = "Bit" desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" +pad = 0 # Auxiliary @@ -32,16 +36,19 @@ desc = "Whether $#`lhs` < #`rhs`$, taking `signed` into account" name = "lhs_sub_rhs" type = "DWordHL" desc = "$#`lhs` - #`rhs`$" +pad = 0 [[variables.auxiliary]] name = "lhs_msb" type = "Bit" desc = "The most significant bit of `lhs`" +pad = 0 [[variables.auxiliary]] name = "rhs_msb" type = "Bit" desc = "The most significant bit of `rhs`" +pad = 0 # Virtual @@ -67,6 +74,7 @@ def = ["idx", "carry", 1] name = "μ" type = "Bit" desc = "" +pad = 0 [[assumptions]] diff --git a/spec/src/shift.toml b/spec/src/shift.toml index e2ddfa12b..ad6172af8 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -6,26 +6,31 @@ name = "SHIFT" name = "in" type = "DWordHL" desc = "The value being shifted" +pad = 0 [[variables.input]] name = "shift" type = "Byte" desc = "Number of bits to shift `in` by." +pad = 0 [[variables.input]] name = "direction" type = "Bit" desc = "Whether to shift left (0) or right (1)." +pad = 0 [[variables.input]] name = "signed" type = "Bit" desc = "Whether to interpret `in` as a signed integer." +pad = 0 [[variables.input]] name = "word_instr" type = "Bit" desc = "Whether this is a Word-instruction (1) or not (0)." +pad = 0 # Output @@ -34,6 +39,7 @@ desc = "Whether this is a Word-instruction (1) or not (0)." name = "out" type = "DWordWL" desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" +pad = 0 # Auxiliary @@ -41,31 +47,37 @@ desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" name = "is_negative" type = "Bit" desc = "Whether `in` is negative" +pad = 0 [[variables.auxiliary]] name = "bit_shift" type = "Byte" desc = "Value by which to shift `in` to obtain `X` and `Y`" +pad = 0 [[variables.auxiliary]] name = "zbs" type = "Bit" desc = "Whether `bit_shift` is zero (1) or not (0)." +pad = 1 [[variables.auxiliary]] name = "X" type = ["Half", 5] desc = "scratch variable." +pad = 0 # TODO: array [[variables.auxiliary]] name = "Y" type = ["Half", 4] desc = "scratch variable." +pad = 0 # TODO: array [[variables.auxiliary]] name = "limb_shift" type = ["Bit", 4] desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod s$, where $s = 2$ when $#`word_instr` = 1$ and $4$ otherwise." +pad = 0 # TODO: array # Virtual @@ -114,6 +126,7 @@ def = {idx="i", range=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i name = "μ" type = "Bit" desc = "" +pad = 0