From af68269163044eb8f1ce8f642e59331e94c18b80 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 10:57:25 +0200 Subject: [PATCH 1/9] spec: add backticks to section titles --- spec/book.typ | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index 38fec945c..bcc5fec19 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,7 +9,7 @@ version: "0.2", summary: ( ("PROOF SYSTEM", ( - ("logup.typ", [LogUp argument], ), + ("logup.typ", [`LogUp` argument], ), ("memory.typ", [Memory argument], ), )), ("OVERVIEW", ( @@ -17,31 +17,31 @@ ("signatures.typ", [Signatures], ), )), ("TEMPLATES", ( - ("is_bit.typ", [IS_BIT template], ), - ("sign.typ", [SIGN template], ), - ("add.typ", [ADD/SUB template], ), - ("neg.typ", [NEG template], ), + ("is_bit.typ", [`IS_BIT` template], ), + ("sign.typ", [`SIGN` template], ), + ("add.typ", [`ADD`/`SUB` template], ), + ("neg.typ", [`NEG` template], ), )), ("MEMORY", ( - ("memw.typ", [MEMW chip], ), + ("memw.typ", [`MEMW` chip], ), )), ("CPU", ( - ("decode.typ", [DECODE table], ), - ("cpu.typ", [CPU chip], ), + ("decode.typ", [`DECODE` table], ), + ("cpu.typ", [`CPU` chip], ), )), ("ALU", ( - ("shift.typ", [SHIFT chip], ), - ("branch.typ", [BRANCH chip], ), - ("lt.typ", [LT chip], ), - ("mul.typ", [MUL chip], ), - ("dvrm.typ", [DVRM chip], ), - ("load.typ", [LOAD chip], ), - ("bitwise.typ", [BITWISE chips], ), + ("shift.typ", [`SHIFT` chip], ), + ("branch.typ", [`BRANCH` chip], ), + ("lt.typ", [`LT` chip], ), + ("mul.typ", [`MUL` chip], ), + ("dvrm.typ", [`DVRM` chip], ), + ("load.typ", [`LOAD` chip], ), + ("bitwise.typ", [`BITWISE` chips], ), )), ("ECALLS", ( - ("about_ecalls.typ", [About ECALL], ), - ("halt.typ", [HALT chip], ), - ("commit.typ", [COMMIT chip], ), + ("about_ecalls.typ", [About `ECALL`], ), + ("halt.typ", [`HALT` chip], ), + ("commit.typ", [`COMMIT` chip], ), )) ) ) From 5217ffdc65a53aafe8b70f00577c0487817be466 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 11:21:21 +0200 Subject: [PATCH 2/9] spec: replace "columns" headers with "variables" --- spec/bitwise.typ | 2 +- spec/branch.typ | 2 +- spec/commit.typ | 2 +- spec/cpu.typ | 2 +- spec/decode.typ | 2 +- spec/dvrm.typ | 2 +- spec/halt.typ | 2 +- spec/load.typ | 2 +- spec/lt.typ | 2 +- spec/memw.typ | 4 ++-- spec/mul.typ | 2 +- spec/shift.typ | 4 ++-- 12 files changed, 14 insertions(+), 14 deletions(-) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 06a2ce822..9764ca996 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -19,7 +19,7 @@ The #bitwise chips deal with precomputed lookup tables for bitwise boolean operations and convenience functionalities over small domains. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_precomputed = ("input", "output").map(c => chip.variables.at(c)).flatten().len() diff --git a/spec/branch.typ b/spec/branch.typ index ee406f2e0..4294ecc91 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -18,7 +18,7 @@ The #branch chip computes the target address of a branching instruction. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/commit.typ b/spec/commit.typ index a5974e763..d0638f2b6 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -16,7 +16,7 @@ #let chip = load_chip("src/commit.toml", config) #let commit = raw(chip.name) -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/cpu.typ b/spec/cpu.typ index c5d693782..ceb49f40f 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -19,7 +19,7 @@ The #cpu chip coordinates memory accesses and dispatches to other chips for arithmetic and logical operations. It bases its decisions on the entry of the `DECODE` table (@decode) corresponding the the current program counter (PC). -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/decode.typ b/spec/decode.typ index f57d7c76f..e88de8b66 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -21,7 +21,7 @@ For reasons of efficiency, data in this table is significantly compressed. Since reasoning about this compressed form is needlessly complex, the `decode (uncompressed)` section presents the same table in uncompressed form, and explains how to decode `RV64IM` assembly instructions to it. Instructions on how to compress the uncompressed table to form the compressed decode table, can be derived from the `packed_decode` variable provided below. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 9afc3ed7f..c054371f0 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -19,7 +19,7 @@ The #dvrm chip provides division and remainder functionality, both signed and unsigned. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/halt.typ b/spec/halt.typ index 803c06e60..0f128c439 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -16,7 +16,7 @@ #let chip = load_chip("src/halt.toml", config) #let halt = raw(chip.name) -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/load.typ b/spec/load.typ index e7d6d3da5..ad3f41f65 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -19,7 +19,7 @@ The #load chip provides functionality to read values from memory and sign-extend them where appropriate. It delegates low-level memory handling to the `MEMW` chip (@memw). -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/lt.typ b/spec/lt.typ index c9e700310..cab787c10 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -18,7 +18,7 @@ The #lt chip constrains an indicator bit for the less-than relation, signed or unsigned. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/memw.typ b/spec/memw.typ index fb5c93e90..89337a655 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -22,7 +22,7 @@ in chunks of 1, 2, 4 or 8 values. It introduces the old value and last-accessed timestamps of memory addresses internally, in order to satisfy the design of the memory argument (@memory). -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_memw_interactions = compute_nr_interactions(chip) @@ -119,7 +119,7 @@ If either of these rules does not apply to your access, you should fall back to Note moreover that this chip does not guard against misaligned register access faults: to access register with a given `address`, one must provide $2 dot #`address`$ in the lookup. -== Columns +== Variables #let nr_variables = total_nr_variables(register_chip) #let nr_columns = total_nr_instantiated_columns(register_chip, config) #let nr_memw_r_interactions = compute_nr_interactions(register_chip) diff --git a/spec/mul.typ b/spec/mul.typ index 479c2f32d..0fec060b1 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -20,7 +20,7 @@ The #mul chip constrains multiplication, both signed and unsigned, as well as providing access to the low and high halfs of the multiplication result. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/shift.typ b/spec/shift.typ index f356122a3..30089091a 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -26,7 +26,7 @@ $ ) $ where -$ +$ #`s` := cases( #`shift` mod 32 "if" #`word_instr` = 1, #`shift` mod 64 "if" #`word_instr` = 0, @@ -34,7 +34,7 @@ $ $ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. -= Columns += Variables #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) From df6d5a51fde10ad23f92e56d12e2ae4f4abef97c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 11:24:44 +0200 Subject: [PATCH 3/9] spec: auto count nr_variables --- spec/is_bit.typ | 5 +++-- spec/sign.typ | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 53a466501..a40c7e0e9 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip -#import "/chip.typ": render_chip_column_table, render_constraint_table, set_nr_interactions +#import "/chip.typ": render_chip_column_table, render_constraint_table, set_nr_interactions, total_nr_variables #let config = load_config() #let chip = load_chip("src/is_bit.toml", config) @@ -8,6 +8,7 @@ #show: book-page(chip.name) #set_nr_interactions(chip) +#let nr_variables = total_nr_variables(chip) #let is_bit = raw(chip.name) @@ -15,7 +16,7 @@ Barring exceptional cases, this template is used to assert that a variable of type `Bit` assumes a valid value under some condition. = Variables -The #is_bit template operates on two variables: `cond` and `X`: +The #is_bit template operates on #nr_variables variables: #render_chip_column_table(chip, config) = Constraints diff --git a/spec/sign.typ b/spec/sign.typ index 9e727e0ac..1ce9914e2 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -15,7 +15,7 @@ It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise. = Variables -The #sign template operates on three variables and introduces #nr_interactions interaction(s): +The #sign template operates on #nr_variables variables and introduces #nr_interactions interaction(s): #render_chip_column_table(chip, config) = Assumptions From 67316975bcef92b94d29290f27e7be9ce54835d7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 11:32:55 +0200 Subject: [PATCH 4/9] spec: standardize "optimizations"-section headers --- spec/bitwise.typ | 2 +- spec/memw.typ | 3 ++- spec/mul.typ | 5 ++--- spec/neg.typ | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 9764ca996..cd23a19b9 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -35,7 +35,7 @@ As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$. This chip adds the following interactions to the lookup: #render_constraint_table(chip, config) -= Areas of Optimization += Notes/Optimizations The following ideas may prove to be optimizations for the #bitwise chip: + Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once. When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`. diff --git a/spec/memw.typ b/spec/memw.typ index 89337a655..a1c5311ae 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -155,7 +155,8 @@ Lastly, this chip contributes the following interactions to the logup: The table can be padded to the next power of two with the following value assignments: #render_chip_padding_table(register_chip, config) -= Future optimization ideas += Notes/optimizations +The following ideas may prove to be optimizations for the #memw/#aligned/#reg chip: - `MEMB` chip that does a one-byte write to remove old_timestamp from here (uncertain tradeoffs) - Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALF` lookups may make some GKR things faster if there are known zeroes. - For the register fast-path, one may upgrade the `IS_HALF` check to an `IS_B20` check for extended range at the cost of looking through a larger table. \ No newline at end of file diff --git a/spec/mul.typ b/spec/mul.typ index 0fec060b1..a25735f31 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -102,11 +102,10 @@ The table can be padded to the next power of two with the following value assign #render_chip_padding_table(chip, config) -= Notes += Notes/optimizations - `lo` and `hi` are stored in `DWordHL`s (rather than `DWordWL`s) because of their values being range checked. Since it is not required that both `μ_lo` and `μ_hi` are non-zero at the same time, one cannot safely assume their range to be checked elsewhere. - - As an optimization, one might be able to use a `DWordWL` and `DWordHL` to store `lo` and `hi`, +- As an optimization, one might be able to use a `DWordWL` and `DWordHL` to store `lo` and `hi`, where one would decide which to store in which based on the multiplicities `μ_lo` and `μ_hi`; the value sent into the lookup could then be assumed range-checked by the other side of the relation. This optimization was not included at this moment because of its negative impact on the readability and verifiability of the chip. diff --git a/spec/neg.typ b/spec/neg.typ index b2f75117a..bf1f91e8c 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -61,7 +61,7 @@ $ when `cond` is set. When `cond` is not set, the two lookups are not executed, allowing `neg` to take any value in either case. -= Note +#par(strong("Note")) It is worth noting that this construction does _not_ require the limbs of `neg` to be range checked, thus allowing it be represented by the unrangecheckable `DWordWL` rather than a `DWordHL`. The input value `x` is still assumed to be range-checked, however. From b60eadc503845c3a7c5d39d88a66fd5e61cad048 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 13:37:18 +0200 Subject: [PATCH 5/9] spec/config: add missing spaces --- spec/src/config.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/config.toml b/spec/src/config.toml index 7e6389e3b..d9dcaec37 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -78,7 +78,7 @@ label = "DWordHHW" subtypes = ["Word", "Half", "Half"] desc = """\ Variable that can only assume values in the range $[0, 2^64)$. \\ - Represented as a `Word` and two `Half` variables.\ + Represented as a `Word` and two `Half` variables. \ The `Word` is the *least* significant digit. """ @@ -87,7 +87,7 @@ label = "DWordWHH" subtypes = ["Half", "Half", "Word"] desc = """\ Variable that can only assume values in the range $[0, 2^64)$. \\ - Represented as a `Word` and two `Half` variables.\ + Represented as a `Word` and two `Half` variables. \ The `Word` is the *most* significant digit. """ From df05367910a089d3b7fa814673a66444b34004c5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 13:57:18 +0200 Subject: [PATCH 6/9] spec/chip: rename *_column_table as *_variable_table --- spec/about_ecalls.typ | 2 +- spec/add.typ | 4 ++-- spec/bitwise.typ | 4 ++-- spec/branch.typ | 4 ++-- spec/chip.typ | 6 +++--- spec/commit.typ | 4 ++-- spec/cpu.typ | 4 ++-- spec/decode.typ | 6 +++--- spec/dvrm.typ | 4 ++-- spec/halt.typ | 6 +++--- spec/is_bit.typ | 4 ++-- spec/load.typ | 4 ++-- spec/lt.typ | 4 ++-- spec/memory.typ | 4 ++-- spec/memw.typ | 8 ++++---- spec/mul.typ | 4 ++-- spec/neg.typ | 4 ++-- spec/shift.typ | 4 ++-- spec/sign.typ | 6 +++--- 19 files changed, 43 insertions(+), 43 deletions(-) diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index d2f55f55a..ef4203610 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, render_constraint_table, diff --git a/spec/add.typ b/spec/add.typ index 7fb5cd43a..0772aa30b 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page, et #import "/src.typ": load_config, load_chip -#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions, +#import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions, #let config = load_config() #let chip = load_chip("src/add.toml", config) @@ -23,7 +23,7 @@ It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expressio = Variables This template introduces #nr_interactions interaction(s). -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index cd23a19b9..82f9e36f9 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, render_constraint_table, @@ -26,7 +26,7 @@ and convenience functionalities over small domains. The #bitwise chip is comprised of #nr_variables variables that are expressed using #nr_columns columns. Of these, the _input_ and _output_ variables (#nr_precomputed in total) are precomputed. -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) *Note*: This table contains one row for every possible value of `(X, Y, Z)`. As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$. diff --git a/spec/branch.typ b/spec/branch.typ index 4294ecc91..0743ae2f9 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, compute_nr_interactions, total_nr_variables, total_nr_instantiated_columns, @@ -24,7 +24,7 @@ The #branch chip computes the target address of a branching instruction. #let nr_interactions = compute_nr_interactions(chip) The #branch chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions diff --git a/spec/chip.typ b/spec/chip.typ index 8304717ff..650d6d2eb 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -145,8 +145,8 @@ ), caption: [Overview of padding values for #chip.name chip.]) } -/// Generates a table listing `chip`'s columns. -#let render_chip_column_table(chip, config) = { +/// Generates a table listing `chip`'s variables. +#let render_chip_variable_table(chip, config) = { // Render a definition's iterators let render_def_iters(iters) = { @@ -235,7 +235,7 @@ } (table.cell(colspan: 4, []), ) }, - ), caption: [Column overview of #chip.name chip.]) + ), caption: [Variable overview of #chip.name chip.]) } #let cref(obj, body) = { diff --git a/spec/commit.typ b/spec/commit.typ index d0638f2b6..a6fea1b6c 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -22,7 +22,7 @@ #let nr_interactions = compute_nr_interactions(chip) The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions: -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Constraints In this VM, committing is considered equivalent to writing a value to `stdout`. diff --git a/spec/cpu.typ b/spec/cpu.typ index ceb49f40f..2fbd60d59 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -25,7 +25,7 @@ It bases its decisions on the entry of the `DECODE` table (@decode) correspondin #let nr_interactions = compute_nr_interactions(chip) The #cpu chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/decode.typ b/spec/decode.typ index e88de8b66..57fb29d73 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, render_constraint_table, @@ -26,7 +26,7 @@ Instructions on how to compress the uncompressed table to form the compressed de #let nr_columns = total_nr_instantiated_columns(chip, config) The #decode table is comprised of #nr_variables variables that are expressed using #nr_columns columns: -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Padding The #decode table must be padded to a length that is a power of two. @@ -46,7 +46,7 @@ Note that the below table is _not_ used in practice: it is solely used for the p #let config = load_config() #let uncompressed_chip = load_chip("src/decode_uncompressed.toml", config) -#render_chip_column_table(uncompressed_chip, config) +#render_chip_variable_table(uncompressed_chip, config) We will illustrate how each instruction should be expressed in this (uncompressed) decoding table. The columns of the accompanying table represent the following: diff --git a/spec/dvrm.typ b/spec/dvrm.typ index c054371f0..1118aa10a 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -25,7 +25,7 @@ The #dvrm chip provides division and remainder functionality, both signed and un #let nr_interactions = compute_nr_interactions(chip) The #dvrm chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/halt.typ b/spec/halt.typ index 0f128c439..691154f61 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -21,8 +21,8 @@ #let nr_columns = total_nr_instantiated_columns(chip, config) #let nr_interactions = compute_nr_interactions(chip) -The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_interactions interactions:: -#render_chip_column_table(chip, config) +The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_interactions interactions: +#render_chip_variable_table(chip, config) = Assumptions It is assumed the input is range checked: diff --git a/spec/is_bit.typ b/spec/is_bit.typ index a40c7e0e9..21c2ee97d 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip -#import "/chip.typ": render_chip_column_table, render_constraint_table, set_nr_interactions, total_nr_variables +#import "/chip.typ": render_chip_variable_table, render_constraint_table, set_nr_interactions, total_nr_variables #let config = load_config() #let chip = load_chip("src/is_bit.toml", config) @@ -17,7 +17,7 @@ Barring exceptional cases, this template is used to assert that a variable of ty = Variables The #is_bit template operates on #nr_variables variables: -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Constraints It takes only one constraint to enforce that `X` must be either $0$ or $1$ whenever $#`cond` eq.not 0$: diff --git a/spec/load.typ b/spec/load.typ index ad3f41f65..ac469ec79 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, render_chip_padding_table, render_constraint_table, compute_nr_interactions, @@ -25,7 +25,7 @@ It delegates low-level memory handling to the `MEMW` chip (@memw). #let nr_interactions = compute_nr_interactions(chip) The #load chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/lt.typ b/spec/lt.typ index cab787c10..2e0ac8be4 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, render_chip_padding_table, render_constraint_table, total_nr_instantiated_columns, @@ -24,7 +24,7 @@ The #lt chip constrains an indicator bit for the less-than relation, signed or u #let nr_interactions = compute_nr_interactions(chip) The #lt chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions We assume the inputs `lhs`, `rhs` and `signed` are partially range checked. diff --git a/spec/memory.typ b/spec/memory.typ index 183bb95fa..876884c85 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, render_chip_padding_table, render_constraint_table, total_nr_instantiated_columns, @@ -168,7 +168,7 @@ We present here a set of constraints on the `PAGE` table that For zero-initialized pages, `init` can be a constant `0`, and hence doesn't need a column, nor a range check. -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) #render_constraint_table(chip, config) diff --git a/spec/memw.typ b/spec/memw.typ index a1c5311ae..425508597 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -2,7 +2,7 @@ #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -28,7 +28,7 @@ in order to satisfy the design of the memory argument (@memory). #let nr_memw_interactions = compute_nr_interactions(chip) The #memw chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_memw_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions @@ -91,7 +91,7 @@ Further logic remains essentially the same, so we briefly present the relevant t #let nr_columns = total_nr_instantiated_columns(alignedchip, config) The #aligned chip only needs #nr_variables variables, expressed through #nr_columns columns; it leverages #nr_aligned_interactions interactions. -#render_chip_column_table(alignedchip, config) +#render_chip_variable_table(alignedchip, config) #render_chip_assumptions(alignedchip, config) #render_constraint_table(alignedchip, config) @@ -125,7 +125,7 @@ Note moreover that this chip does not guard against misaligned register access f #let nr_memw_r_interactions = compute_nr_interactions(register_chip) The #reg chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_memw_r_interactions interactions: -#render_chip_column_table(register_chip, config) +#render_chip_variable_table(register_chip, config) == Assumptions The following range checks are assumed to be performed/enforced outside of this chip: diff --git a/spec/mul.typ b/spec/mul.typ index a25735f31..6e6de12e0 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -26,7 +26,7 @@ as well as providing access to the low and high halfs of the multiplication resu #let nr_interactions = compute_nr_interactions(chip) The #mul chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) #let stackrel(top, bottom) = { $mat(delim: #none, top; bottom)$ diff --git a/spec/neg.typ b/spec/neg.typ index bf1f91e8c..ce202d668 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page, et #import "/src.typ": load_config, load_chip -#import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table, compute_nr_interactions, +#import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, compute_nr_interactions, #let config = load_config() #let chip = load_chip("src/neg.toml", config) @@ -15,7 +15,7 @@ It requires `cond` to be a bit. = Variables This template introduces #nr_interactions interaction(s). -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/shift.typ b/spec/shift.typ index 30089091a..c464d5d55 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -1,7 +1,7 @@ #import "/book.typ": book-page, et #import "/src.typ": load_config, load_chip #import "/chip.typ": ( - render_chip_column_table, + render_chip_variable_table, total_nr_variables, total_nr_instantiated_columns, compute_nr_interactions, @@ -40,7 +40,7 @@ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while #let nr_interactions = compute_nr_interactions(chip) The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +#render_chip_variable_table(chip, config) = Assumptions #render_chip_assumptions(chip, config) diff --git a/spec/sign.typ b/spec/sign.typ index 1ce9914e2..14a6e4000 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -1,6 +1,6 @@ #import "/book.typ": book-page #import "/src.typ": load_config, load_chip -#import "/chip.typ": render_chip_column_table, total_nr_variables, render_chip_assumptions, render_constraint_table, compute_nr_interactions, +#import "/chip.typ": render_chip_variable_table, total_nr_variables, render_chip_assumptions, render_constraint_table, compute_nr_interactions, #let config = load_config() #let chip = load_chip("src/sign.toml", config) @@ -15,8 +15,8 @@ It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise. = Variables -The #sign template operates on #nr_variables variables and introduces #nr_interactions interaction(s): -#render_chip_column_table(chip, config) +The #sign template introduces #nr_interactions interaction(s): +#render_chip_variable_table(chip, config) = Assumptions The #sign template operates on the following assumptions: From 8c67394263692af3c1e97074c3159d02049dccf6 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 7 Apr 2026 13:52:17 +0200 Subject: [PATCH 7/9] spec: drop table captions --- spec/chip.typ | 8 ++++---- spec/decode.typ | 4 +--- spec/signatures.typ | 14 ++++---------- 3 files changed, 9 insertions(+), 17 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 650d6d2eb..f3e0892f7 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -142,7 +142,7 @@ ([#raw(var.name)], [$:=$], [#expr_to_math(var.pad)],) } }, - ), caption: [Overview of padding values for #chip.name chip.]) + )) } /// Generates a table listing `chip`'s variables. @@ -235,7 +235,7 @@ } (table.cell(colspan: 4, []), ) }, - ), caption: [Variable overview of #chip.name chip.]) + )) } #let cref(obj, body) = { @@ -278,7 +278,7 @@ ..for assumption in chip.assumptions { ([#tag(assumption)], [#iters(assumption)], [#eval(assumption.desc, mode: "markup")]) }, - ), caption: [Assumption overview of #chip.name chip.]) + )) } /// Generates a table listing all interactions initiated by `chip`'s. @@ -389,5 +389,5 @@ } } } - ), caption: [Constraint overview of #chip.name chip.]) + )) } diff --git a/spec/decode.typ b/spec/decode.typ index 57fb29d73..bb5d0d5a1 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -93,9 +93,7 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is ..lines.flatten(), table.hline(stroke: 1.5pt), table.footer([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*]), - ), - caption: [Decoding table] - ) + )) } #let decoding = ( diff --git a/spec/signatures.typ b/spec/signatures.typ index 5673cdcf6..12d84f757 100644 --- a/spec/signatures.typ +++ b/spec/signatures.typ @@ -56,8 +56,7 @@ #let interactions = signatures.signatures.filter(s => s.kind == "interaction") The following lists signatures of the #interactions.len() interactions in this VM. -#figure( - table( +#figure(table( columns: (1fr, auto), inset: 7pt, align: (top+left, center), @@ -68,14 +67,11 @@ The following lists signatures of the #interactions.len() interactions in this V ..for sig in interactions { ([#render_signature(sig)], [#interaction_bus_size(sig)]) }, - ), - caption: "Signature overview of interactions", -) +)) #let templates = signatures.signatures.filter(s => s.kind == "template") Below, we list the signatures of the #templates.len() templates in this VM. -#figure( - table( +#figure(table( columns: 1fr, inset: 7pt, align: (top+left, center), @@ -85,6 +81,4 @@ Below, we list the signatures of the #templates.len() templates in this VM. ..for sig in templates { ([#render_signature(sig)], ) }, - ), - caption: "Signature overview of templates", -) +)) From 36ba98f637815cb5188bbcde300a16aaef0a16d4 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 9 Apr 2026 10:23:48 +0200 Subject: [PATCH 8/9] spec/v0.2: turn note into aside --- spec/neg.typ | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/spec/neg.typ b/spec/neg.typ index ce202d668..e33375b61 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, et +#import "/book.typ": book-page, aside, et #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, compute_nr_interactions, @@ -61,7 +61,8 @@ $ when `cond` is set. When `cond` is not set, the two lookups are not executed, allowing `neg` to take any value in either case. -#par(strong("Note")) -It is worth noting that this construction does _not_ require the limbs of `neg` to be range checked, -thus allowing it be represented by the unrangecheckable `DWordWL` rather than a `DWordHL`. -The input value `x` is still assumed to be range-checked, however. +#aside("Missing range check?")[ + It is worth noting that this construction does _not_ require the limbs of `neg` to be range checked, + thus allowing it be represented by the unrangecheckable `DWordWL` rather than a `DWordHL`. + The input value `x` is still assumed to be range-checked, however. +] From 42128e739955530375ce123f98c73bf1aab4eabd Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 10 Apr 2026 11:40:53 +0200 Subject: [PATCH 9/9] spec: place correctness arguments in separate section --- spec/is_bit.typ | 2 +- spec/neg.typ | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 21c2ee97d..5246a623a 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -27,7 +27,7 @@ It takes only one constraint to enforce that `X` must be either $0$ or $1$ whene - As described earlier, the `cond` variable must be describable by a degree-1 (i.e., linear) expression. This is to make sure that @isbit:c:isbit's expression has degree at most 3. -= Proof of correctness +== Correctness argument If `cond` is $0$, @isbit:c:isbit is trivially satisfied: `X` can assume any value and the polynomial constraint will evaluate to $0$ regardless. When $#`cond` eq.not 0$, it follows that the statement can only be proven when $#`X` (1-#`X`) equiv 0 mod p$, with $p$ the modulus of the field. Because `BaseField` is a prime field, this equality is only satisfied if either $#`X` equiv 0 mod p$ or $1-#`X` equiv 0 mod p$. diff --git a/spec/neg.typ b/spec/neg.typ index e33375b61..336152892 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -23,6 +23,8 @@ This template introduces #nr_interactions interaction(s). = Constraints We constrain this equality using two constraints: #render_constraint_table(chip, config) + +== Correctness argument The constraints force the `carry` values to be fixed. Writing `carry`'s definition, we then find that $