spec: Cleanup, uniformize chapters, make colors work better on web.

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))
-}
-
-#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<sum; lhs, rhs>"))
-where `cond` is any value described by an expression _of degree at most $1$_.
-#highlighted_code("ADD<sum; lhs, rhs>") 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<diff; lhs, rhs>"))
-maps onto the #add template as 
-#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(230), raw("cond => ADD<lhs; rhs, diff>"))
-It constrains that $#`diff` = #`lhs` - #`rhs` mod 2^64$ when the expression `cond` is non-zero.
-As with #add, #highlighted_code("SUB<diff; lhs, rhs>") can be used to denote the _unconditional_ application of the template.
+
+#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<diff; lhs, rhs>` := #`ADD<lhs; rhs, diff>`,
+$
+in both conditional and unconditional versions.
+It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero.
 
 = Variables
 #render_chip_column_table(chip, config)

spec/bitwise.typ

@@ -14,6 +14,10 @@
 #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
+and convenience functionalities over small domains.
 
 = Columns
 #let nr_variables = total_nr_variables(chip)

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
 }
 
@@ -46,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)
 ])
@@ -83,10 +80,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.
@@ -102,7 +98,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
@@ -140,7 +136,6 @@
   if is-shiroa {
     (body) => {
       show: common-formatting
-      context _xref-included.update(x => x + ((file): true))
       context _toplevel.update(s => {
         if s == none {
           file
@@ -153,6 +148,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
       ])
     }

spec/branch.typ

@@ -13,6 +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.
 
 = Columns
 #let nr_variables = total_nr_variables(chip)
@@ -27,7 +30,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.
 

spec/cpu.typ

@@ -13,6 +13,10 @@
 #let chip = load_chip("src/cpu.toml", config)
 
 #show: book-page(chip.name)
+#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).
 
 = Columns
 #let nr_variables = total_nr_variables(chip)
@@ -29,8 +33,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.

spec/decode.typ

@@ -79,13 +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) =>
-      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(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),

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)

spec/ebook.typ

@@ -1,17 +1,14 @@
-#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()
 
 #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)

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, 

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<X>"))
-where `cond` is any value described by an expression _of degree at most $1$_.
-Note that #highlighted_code("IS_BIT<X>") 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)

spec/load.typ

@@ -13,6 +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 low-level memory handling to the `MEMW` chip (@memw).
 
 = Columns
 #let nr_variables = total_nr_variables(chip)

spec/lt.typ

@@ -13,6 +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.
 
 = Columns
 #let nr_variables = total_nr_variables(chip)

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.
 

spec/memw.typ

@@ -13,6 +13,13 @@
 
 #show: book-page(chip.name)
 
+#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).
+
 = Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)

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.
+  This optimization was not included at this moment because of its negative impact on the readability and verifiability of the chip.

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<neg; x>"))
-where `cond` is a bit value (i.e., lies in ${0, 1}$)  described by an expression _of degree at most $1$_.
-#highlighted_code("NEG<neg; x>") 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)

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,