spec: Add support for specifying padding values of columns

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)

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) = {
 

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)

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")
+#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)

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)

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]]

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"]

spec/src/lt.toml

@@ -7,23 +7,27 @@ 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
 
 [[variables.output]]
 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]]

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,38 +39,45 @@ 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
 
 [[variables.auxiliary]]
 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