From 062054bd729b94de07aae1ecf50de27b1b09f9b2 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 13 Feb 2026 16:49:45 +0100 Subject: [PATCH 1/6] spec: Cleanup, uniformize chapters, make colors work better on web. --- spec/add.typ | 30 ++++++------------------------ spec/bitwise.typ | 3 +++ spec/book.typ | 1 + spec/branch.typ | 3 ++- spec/cpu.typ | 5 +++-- spec/decode.typ | 5 +++-- spec/dvrm.typ | 2 ++ spec/ebook.typ | 1 + spec/ecall.typ | 9 +++++---- spec/is_bit.typ | 15 --------------- spec/load.typ | 3 +++ spec/lt.typ | 2 ++ spec/memory.typ | 8 +++----- spec/memw.typ | 5 +++++ spec/mul.typ | 5 ++++- spec/neg.typ | 16 +--------------- spec/shift.typ | 15 +-------------- spec/sign.typ | 13 ------------- spec/src/config.toml | 2 +- 19 files changed, 46 insertions(+), 97 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index 241ea8621..333a7407f 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -8,33 +8,15 @@ #show: book-page(chip.name) #let add = raw(chip.name) - -#let highlighted_code(code) = { - box( - inset: (left: 4pt, right: 4pt), - outset: (top: 4pt, bottom: 4pt), - radius: 2pt, - fill: luma(230), - raw(code)) -} +#let sub = raw("SUB") #add is a constraint template that is used to assert that $#`sum` = #`lhs` + #`rhs` mod 2^64$, under the condition that `cond` is non-zero. - -= Notation -The #add constraint template has the following interface: -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD")) -where `cond` is any value described by an expression _of degree at most $1$_. -#highlighted_code("ADD") can be used to denote the _unconditional_ application of the #add template to `lhs`, `rhs`, and `sum`. - -#let sub = raw("SUB") -== #sub -For ease of notation, we moreover introduce the #sub constraint template. -Its interface -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => SUB")) -maps onto the #add template as -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD")) +For ease of notation, we moreover introduce the #sub constraint template +$ +#`SUB` colon.eq #`ADD`, +$ +in both conditional and unconditional versions. It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero. -As with #add, #highlighted_code("SUB") can be used to denote the _unconditional_ application of the template. = Variables #render_chip_column_table(chip, config) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index ef1e3a671..d0cd68ca3 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -15,6 +15,9 @@ #show: book-page(chip.name) +The bitwise chips deal with precomputed lookup tables for bitwise boolean operations +and convenience functionalities over small domains. + = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/book.typ b/spec/book.typ index 7a55323cd..fef730acb 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -35,6 +35,7 @@ #let common-formatting(body) = { set footnote(numbering: "[1]") + show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) body } diff --git a/spec/branch.typ b/spec/branch.typ index 3e944ca63..9212223d8 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -14,6 +14,8 @@ #show: book-page(chip.name) +The BRANCH chip computes the target address of a branching instruction. + = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -27,7 +29,6 @@ The `BRANCH` chip is comprised of #nr_variables variables that are expressed usi = Constraints -#rj[Check correspondence with CPU for passing in `offset` as word or dword] We constrain `next_pc` to be $#`base_address` + #`offset`$, where `base_address` equals `pc` when $#`JALR` = 0$ and `register` otherwise. diff --git a/spec/cpu.typ b/spec/cpu.typ index ed6126388..dbc233667 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -14,6 +14,9 @@ #show: book-page(chip.name) +The CPU chip is 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 #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -29,8 +32,6 @@ First, we perform a decoding lookup for the current PC. #render_constraint_table(chip, config, groups: "decode") -#rj[All casts for interactions will have to be reviewed once other chip interfaces stabilise] - == Range checks We constrain all columns to have the appropriate ranges. diff --git a/spec/decode.typ b/spec/decode.typ index 87f6083f5..64ba7ce47 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -84,8 +84,9 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is inset: (right: .5em), align: (left, right, center, center, left, right), fill: (_, y) => - if calc.odd(y) and y <= lines.len() { luma(245) } - else { white }, + // Overlay a low-opacity fill color to distinguish the different rows better + if calc.odd(y) and y <= lines.len() { color.rgb(0, 0, 100, 20) } + else { color.rgb(0, 0, 0, 0) }, table.header([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*], []), table.hline(stroke: 1.5pt), table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 54e71d771..920aec075 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -17,6 +17,8 @@ #let dvrm = raw(chip.name) +The #dvrm chip provides division and remainder functionality, both signed and unsigned. + = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/ebook.typ b/spec/ebook.typ index e1b15253e..cfd25a36c 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -12,6 +12,7 @@ #show: common-formatting #show heading: set heading(numbering: "1.1") +#show raw.where(block: true): set block(fill: luma(230)) #meta.summary.map(((ch, title, ref)) => [ #pagebreak(weak: true) diff --git a/spec/ecall.typ b/spec/ecall.typ index dd3544ef3..3b82019db 100644 --- a/spec/ecall.typ +++ b/spec/ecall.typ @@ -12,7 +12,9 @@ #let config = load_config() #show: book-page("ecall.typ") -= About `ECALL` + +ECALLs provide system-level functionalities to the guest program. + When `ECALL` is executed, it is assumed that: - register `A7` contains the system call number #footnote([The RISC-V system call ABI; libriscv.no, #link("https://web.archive.org/web/20260128152107/https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[src]]]), @@ -90,12 +92,11 @@ This is why @commit:c:receive_ecall has multiplicity $-#`first`$. The `write` operation --- writing to a file descriptor --- has the following signature: #footnote([Linux man-page on `write`; man7.org, version 6.16, 2025-10-29. #link("https://man7.org/linux/man-pages/man2/write.2.html")[[src]]]) -#[ -#show raw.where(block: true): it => block(it, fill: luma(230), inset: 1em, width: 100%, radius: 5pt) + ```c ssize_t write(size_t count; int fd, const void buf[count], size_t count); ``` -] + That is to say, - `A0` contains the file descriptor, - `A1` contains the address of `buf`'s first byte, diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 33477d377..b09242fe4 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -9,24 +9,9 @@ #let is_bit = raw(chip.name) -#let highlighted_code(code) = { - box( - inset: (left: 4pt, right: 4pt), - outset: (top: 4pt, bottom: 4pt), - radius: 2pt, - fill: luma(230), - raw(code)) -} - #is_bit is a constraint template that is used to assert that a variable lies in the range ${0, 1}$ if some second variable is non-zero. Barring exceptional cases, this template is used to assert that a variable of type `Bit` assumes a valid value under some condition. -= Interface -The #is_bit constraint template has the following interface: -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => IS_BIT")) -where `cond` is any value described by an expression _of degree at most $1$_. -Note that #highlighted_code("IS_BIT") can be used to denote the _unconditional_ application of the #is_bit template to `X`. - = Variables The #is_bit template operates on two variables: `cond` and `X`: #render_chip_column_table(chip, config) diff --git a/spec/load.typ b/spec/load.typ index bccb830f8..cfe5aaf42 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -14,6 +14,9 @@ #show: book-page(chip.name) +The LOAD chip provides functionality to read values from memory and sign-extend them where appropriate. +It delegates to the MEMW chip (@memw) for lower level memory handling. + = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/lt.typ b/spec/lt.typ index 3447efd70..496730505 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -14,6 +14,8 @@ #show: book-page(chip.name) +The LT chip constrains an indicator bit for the less-than relation, signed or unsigned. + = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/memory.typ b/spec/memory.typ index 62059de37..373bda206 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -107,7 +107,8 @@ This raises the question of how to represent timestamps and cleanly perform this as over a finite field the “less than” relation is ill-defined (though it is common and natural to consider it as the less than relation over the natural lift of the field into the integers). We choose to represent timestamps as machine words, using the existing `LT` chip (@lt) functionality for comparisons. -#rj[Properly link/refer to the LT chip] +The full implementation of the timestamp system can be seen in the `timestamp` column of the CPU (@cpu) and MEMW chips (@memw). +The CPU merely passes in the current timestamp, while MEMW can recall the previously written timestamp and constrain the correct sequencing. #aside[Note on options and trade-offs for timestamp representation][ #grid(columns: (1fr, 1fr), gutter: 1em)[#align(center, emph[Machine word])][#align(center, emph[Field element])][ @@ -123,8 +124,6 @@ We choose to represent timestamps as machine words, using the existing `LT` chip ] ] -#rj[reference to CPU chip/timestamp column and MEMW chip] - = Initialization and Finalization Because the LogUp argument handling token consumption and emission needs to be fully balanced @@ -213,11 +212,10 @@ and hence doesn't need a column, nor a range check. == Register initialization/finalization -#rj[Properly link/reference ECALL/HALT chip] The initial and final state of registers can be entirely known by the verifier, since the relevant initialization values are either zero, or embedded in the ELF, and the final values can be set to a known value -by the HALT ecall. +by the HALT ecall (@ecall). As additionally, the number of registers is small, the verifier can directly add the required balancing terms to the LogUp sum. diff --git a/spec/memw.typ b/spec/memw.typ index 6c12f00a7..94cff421a 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -13,6 +13,11 @@ #show: book-page(chip.name) +The MEMW chip is used to read and write memory locations (both RAM and registers) +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 #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/mul.typ b/spec/mul.typ index a2fb7d1fc..68ab4a2b8 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -16,6 +16,9 @@ #let mul = raw(chip.name) +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 #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -104,4 +107,4 @@ The table can be padded to the next power of two with the following value assign 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. \ No newline at end of file + 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 ac8554689..d700892cb 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -8,22 +8,8 @@ #let neg = raw(chip.name) -#let highlighted_code(code) = { - box( - inset: (left: 4pt, right: 4pt), - outset: (top: 4pt, bottom: 4pt), - radius: 2pt, - fill: luma(230), - raw(code)) -} - #neg is a constraint template that is used to assert that $#`neg` = -#`x`$, under the condition that `cond` is non-zero. - -= Notation -The #neg constraint template has the following interface: -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => NEG")) -where `cond` is a bit value (i.e., lies in ${0, 1}$) described by an expression _of degree at most $1$_. -#highlighted_code("NEG") can be used to denote the _unconditional_ application of the #neg template to `x` and `neg` (which is equivalent to $#`cond` = 1$). +It requires `cond` to be a bit. = Variables #render_chip_column_table(chip, config) diff --git a/spec/shift.typ b/spec/shift.typ index a2a3ec968..b705adb32 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -16,20 +16,7 @@ #show: book-page(chip.name) -= Interface -The #shift chip has the following interface: -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(240), -``` -// param in: the value being shifted -// param shift: the number of bits to shift `in` by -// param direction: whether to shift left (0) or right (1) -// param signed: whether to interpret `in` as a signed (1) or unsigned (0) integer -// param word_instr: whether to execute the SLL/SR* (0) or SLLW/SR*W (1) instruction -// out shifted: the resulting value -SHIFT[shifted: DWord; in: DWord, shift: Byte, direction: Bit, signed: Bit, word_instr: Bit] -``` -) -In other words, the #shift chip is designed to constrain that +The #shift chip is designed to constrain that $ #`shifted` := cases( #`in` #`<<` #`s` " if" #`direction` = 0, diff --git a/spec/sign.typ b/spec/sign.typ index dcc941e47..fc1b8d0a5 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -9,20 +9,7 @@ #let sign = raw(chip.name) -#let highlighted_code(code) = { - box( - inset: (left: 4pt, right: 4pt), - outset: (top: 4pt, bottom: 4pt), - radius: 2pt, - fill: luma(230), - raw(code)) -} - #sign is a constraint template that is used to extract a `Half`word's sign. - -= Interface -The #sign constraint template has the following interface: -#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("SIGN")) It constrains that `sign` is set to `1` when both `X`'s most significant bit and `signed` are $1$, and $0$ otherwise. = Variables diff --git a/spec/src/config.toml b/spec/src/config.toml index fd0885d40..7e6389e3b 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -110,7 +110,7 @@ desc = """\ [[variables.types]] 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." +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 (@cpu), see there for more details about the magic number." preprocessed = true [[variables.types]] From a1dd24d091c68258d6a3071cc38bb89230a3def3 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 13 Feb 2026 18:07:40 +0100 Subject: [PATCH 2/6] Fix double scroll bar --- spec/book.typ | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index fef730acb..da57c4d21 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -84,10 +84,9 @@ // Invisibly include another chapter, so that its labels can be resolved #let xref-include(f) = { - context if f not in _xref-included.get() { - hide(box(width: 0%, height: 0%, strip-all(include "/" + f))) + context { + place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) } - context _xref-included.update(x => x + ((f): true)) } // Generate a cross-link for references to other chapters. @@ -103,7 +102,7 @@ } else { // Because shiroa does weird url escaping let shiroa-label = label(str(lbl).replace(":", "%3A")) - xref-include(ch) + context _xref-included.update(x => x + ((ch): true)) // The ideal would be to use `rf` directly as content argument to `cross-link`, // as that would inherit any/all formatting of the ref we want or need. // Unfortunately the ref link seems to take precedence over the cross-link hyperlink @@ -141,7 +140,6 @@ if is-shiroa { (body) => { show: common-formatting - context _xref-included.update(x => x + ((file): true)) context _toplevel.update(s => { if s == none { file @@ -154,6 +152,9 @@ #show ref: it => context if _toplevel.final() == file { xref(it) } + #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { + xref-include(key) + }).join() #body ]) } From e0cb4b39c74213da1aaa022f2add02bf5840d890 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 13 Feb 2026 18:07:50 +0100 Subject: [PATCH 3/6] Improve decode table --- spec/decode.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/decode.typ b/spec/decode.typ index 64ba7ce47..f57d7c76f 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -79,14 +79,14 @@ To indicate an instruction is provided in compressed form, the `c_type` flag is show figure: set block(breakable: true) figure(table( - columns: (auto, auto, 40pt, 40pt, 1fr, 15pt), + columns: (auto, auto, auto, auto, 1fr, auto), stroke: 0pt, inset: (right: .5em), align: (left, right, center, center, left, right), fill: (_, y) => // Overlay a low-opacity fill color to distinguish the different rows better if calc.odd(y) and y <= lines.len() { color.rgb(0, 0, 100, 20) } - else { color.rgb(0, 0, 0, 0) }, + else { color.rgb(255, 255, 255, 20) }, table.header([*Operation*], [*op-flag*], [*`w_instr`*], [*`signed`*], [*other*], []), table.hline(stroke: 1.5pt), table.vline(x: 1, start: 1, end: lines.len() + 1, stroke: .5pt), From 9c4025be74ecc4727fd00a45f4142398f03e4df9 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 16 Feb 2026 11:35:54 +0100 Subject: [PATCH 4/6] Remove `style` state and make aside box grey. Having multiple web themes makes the style approach almost always wrong, since we cannot rely on the scheme being dark or light, in contrast to a regular PDF. --- spec/book.typ | 8 ++------ spec/ebook.typ | 6 +----- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index da57c4d21..338b2679b 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -47,16 +47,12 @@ #let rj = todo.with(background: teal, name: "Robin") #let et = todo.with(background: rgb("d4aa3a"), name: "Erik") -#let style = state("style", ( - foreground: white, -)) - #let aside(title, body) = context figure( - block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: style.final().foreground, breakable: false)[ + block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false)[ #block(inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), width: 100% + 2em, fill: rgb("55aaff"), - stroke: style.final().foreground, + stroke: luma(50%), align(center, strong(text(fill: black, title)))) #align(left, body) ]) diff --git a/spec/ebook.typ b/spec/ebook.typ index cfd25a36c..0e08536fd 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -1,11 +1,7 @@ -#import "/book.typ": style, meta, common-formatting +#import "/book.typ": meta, common-formatting #set document(author: meta.authors, title: meta.title) -#style.update(( - foreground: black, -)) - #align(center, title(meta.title)) #pagebreak(weak: true) #outline() From 7422cfa9daa5bf809caf6fc62bbcab3b265460c2 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 16 Feb 2026 11:43:17 +0100 Subject: [PATCH 5/6] Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/add.typ | 6 +++--- spec/bitwise.typ | 3 ++- spec/branch.typ | 3 ++- spec/cpu.typ | 3 ++- spec/load.typ | 5 +++-- spec/lt.typ | 3 ++- spec/memory.typ | 6 +++--- spec/memw.typ | 4 +++- 8 files changed, 20 insertions(+), 13 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index 333a7407f..d2afb1788 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -10,13 +10,13 @@ #let add = raw(chip.name) #let sub = raw("SUB") -#add is a constraint template that is used to assert that $#`sum` = #`lhs` + #`rhs` mod 2^64$, under the condition that `cond` is non-zero. +#add is a constraint template that is used to assert that $#`sum` equiv #`lhs` + #`rhs` (mod 2^64)$, under the condition that `cond` is non-zero. For ease of notation, we moreover introduce the #sub constraint template $ -#`SUB` colon.eq #`ADD`, +#`SUB` := #`ADD`, $ in both conditional and unconditional versions. -It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero. +It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero. = Variables #render_chip_column_table(chip, config) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index d0cd68ca3..d0b3d89e2 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -14,8 +14,9 @@ #let bitwise = raw(chip.name) #show: book-page(chip.name) +#let bitwise = raw(chip.name) -The bitwise chips deal with precomputed lookup tables for bitwise boolean operations +The #bitwise chips deal with precomputed lookup tables for bitwise boolean operations and convenience functionalities over small domains. = Columns diff --git a/spec/branch.typ b/spec/branch.typ index 9212223d8..90503e862 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -13,8 +13,9 @@ #let chip = load_chip("src/branch.toml", config) #show: book-page(chip.name) +#let branch = raw(chip.name) -The BRANCH chip computes the target address of a branching instruction. +The #branch chip computes the target address of a branching instruction. = Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/cpu.typ b/spec/cpu.typ index dbc233667..366988952 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -13,8 +13,9 @@ #let chip = load_chip("src/cpu.toml", config) #show: book-page(chip.name) +#let cpu = raw(chip.name) -The CPU chip is coordinates memory accesses and dispatches to other chips for arithmetic and logical operations. +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 diff --git a/spec/load.typ b/spec/load.typ index cfe5aaf42..b12e1c04d 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -13,9 +13,10 @@ #let chip = load_chip("src/load.toml", config) #show: book-page(chip.name) +#let load = raw(chip.name) -The LOAD chip provides functionality to read values from memory and sign-extend them where appropriate. -It delegates to the MEMW chip (@memw) for lower level memory handling. +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 #let nr_variables = total_nr_variables(chip) diff --git a/spec/lt.typ b/spec/lt.typ index 496730505..8e55b390b 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -13,8 +13,9 @@ #let chip = load_chip("src/lt.toml", config) #show: book-page(chip.name) +#let lt = raw(chip.name) -The LT chip constrains an indicator bit for the less-than relation, signed or unsigned. +The #lt chip constrains an indicator bit for the less-than relation, signed or unsigned. = Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/memory.typ b/spec/memory.typ index 373bda206..778183dab 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -107,8 +107,8 @@ This raises the question of how to represent timestamps and cleanly perform this as over a finite field the “less than” relation is ill-defined (though it is common and natural to consider it as the less than relation over the natural lift of the field into the integers). We choose to represent timestamps as machine words, using the existing `LT` chip (@lt) functionality for comparisons. -The full implementation of the timestamp system can be seen in the `timestamp` column of the CPU (@cpu) and MEMW chips (@memw). -The CPU merely passes in the current timestamp, while MEMW can recall the previously written timestamp and constrain the correct sequencing. +The full implementation of the timestamp system can be seen in the `timestamp` column of the `CPU` (@cpu) and `MEMW` chips (@memw). +The `CPU` merely passes in the current timestamp, while `MEMW` can recall the previously written timestamp and constrain the correct sequencing. #aside[Note on options and trade-offs for timestamp representation][ #grid(columns: (1fr, 1fr), gutter: 1em)[#align(center, emph[Machine word])][#align(center, emph[Field element])][ @@ -215,7 +215,7 @@ and hence doesn't need a column, nor a range check. The initial and final state of registers can be entirely known by the verifier, since the relevant initialization values are either zero, or embedded in the ELF, and the final values can be set to a known value -by the HALT ecall (@ecall). +by the `HALT` ecall (@ecall). As additionally, the number of registers is small, the verifier can directly add the required balancing terms to the LogUp sum. diff --git a/spec/memw.typ b/spec/memw.typ index 94cff421a..4b644218a 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -13,7 +13,9 @@ #show: book-page(chip.name) -The MEMW chip is used to read and write memory locations (both RAM and registers) +#let memw = raw(chip.name) + +The #memw chip is used to read and write memory locations (both RAM and registers) 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). From 8fa2b564f07064e494bfde60bc859f8a4588895f Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 17 Feb 2026 14:38:31 +0100 Subject: [PATCH 6/6] Update spec/cpu.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/cpu.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/cpu.typ b/spec/cpu.typ index 366988952..08fe1533d 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -16,7 +16,7 @@ #let cpu = raw(chip.name) 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). +It bases its decisions on the entry of the `DECODE` table (@decode) corresponding the the current program counter (PC). = Columns #let nr_variables = total_nr_variables(chip)