From 35e60f3fc092d342355d4fbe838276e8feb4fa06 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 11:30:30 +0100 Subject: [PATCH 1/5] spec: Add support for specifying padding values of columns --- spec/branch.typ | 6 ++++++ spec/chip.typ | 27 +++++++++++++++++++++++++++ spec/lt.typ | 11 +++++++++-- spec/shift.typ | 7 +++++++ spec/src/branch.toml | 8 ++++++++ spec/src/config.toml | 1 + spec/src/cpu.toml | 1 + spec/src/lt.toml | 8 ++++++++ spec/src/shift.toml | 13 +++++++++++++ 9 files changed, 80 insertions(+), 2 deletions(-) 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..d4aff8fb8 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,6 +24,33 @@ .sum() } +#let render_chip_padding_table(chip, config) = { + 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 (cat, vars) in chip.variables.pairs() { + if cat not in config.variables.categories.instantiated { + continue + } + for var in vars { + if config.variables.types.filter(t => t.label == var.type).all(t => t.at("preprocessed", default: false)) { + continue + } + ( + [#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/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..c05d22697 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: 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 b66639e2a..9741d7b67 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -94,6 +94,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/cpu.toml b/spec/src/cpu.toml index 562a657d0..96c40b7ac 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -1,3 +1,4 @@ +# TODO: padding name = "CPU" 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 From c3fe899f08c052541c6d2562c333511ba7509e92 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 15:09:41 +0100 Subject: [PATCH 2/5] Update spec/chip.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/chip.typ | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index d4aff8fb8..ab709c404 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -25,27 +25,26 @@ } #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.header([*Column*], [], [*Padding value*]), table.hline(stroke: stroke(thickness: 2pt)), - ..for (cat, vars) in chip.variables.pairs() { - if cat not in config.variables.categories.instantiated { - continue - } - for var in vars { - if config.variables.types.filter(t => t.label == var.type).all(t => t.at("preprocessed", default: false)) { - continue - } - ( - [#raw(var.name)], - [$:=$], - [#expr_to_math(var.pad)], - ) + ..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.]) From 088d99e9b17e9734b4e3d6b3faa7dcbff423d610 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 15:11:58 +0100 Subject: [PATCH 3/5] Padding table for MUL --- spec/mul.typ | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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) From e46729be0f7355d722865cd93becd130545d0c59 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 16:22:35 +0100 Subject: [PATCH 4/5] Update spec/src/branch.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/branch.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/branch.toml b/spec/src/branch.toml index c05d22697..d6620dcfd 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -34,7 +34,7 @@ pad = 0 name = "next_pc_high" type = ["Half", 3] desc = "The upper part of the next pc" -pad = 0 # TODO: improve handling for arrays +pad = 0 # TODO(#128): improve handling for arrays [[variables.output]] name = "next_pc_low" From 7936ae57b70b3c899a49fbc0ceab08fd417cf15b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 16:23:16 +0100 Subject: [PATCH 5/5] Update spec/src/cpu.toml Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/cpu.toml | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 96c40b7ac..562a657d0 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -1,4 +1,3 @@ -# TODO: padding name = "CPU"