diff --git a/spec/add.typ b/spec/add.typ
index 241ea8621..d2afb1788 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))
-}
-
-#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)
diff --git a/spec/bitwise.typ b/spec/bitwise.typ
index ef1e3a671..d0b3d89e2 100644
--- a/spec/bitwise.typ
+++ b/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)
diff --git a/spec/book.typ b/spec/book.typ
index 7a55323cd..338b2679b 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
 }
 
@@ -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
       ])
     }
diff --git a/spec/branch.typ b/spec/branch.typ
index 3e944ca63..90503e862 100644
--- a/spec/branch.typ
+++ b/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.
 
diff --git a/spec/cpu.typ b/spec/cpu.typ
index ed6126388..08fe1533d 100644
--- a/spec/cpu.typ
+++ b/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.
diff --git a/spec/decode.typ b/spec/decode.typ
index 87f6083f5..f57d7c76f 100644
--- a/spec/decode.typ
+++ b/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),
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..0e08536fd 100644
--- a/spec/ebook.typ
+++ b/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)
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<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)
diff --git a/spec/load.typ b/spec/load.typ
index bccb830f8..b12e1c04d 100644
--- a/spec/load.typ
+++ b/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)
diff --git a/spec/lt.typ b/spec/lt.typ
index 3447efd70..8e55b390b 100644
--- a/spec/lt.typ
+++ b/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)
diff --git a/spec/memory.typ b/spec/memory.typ
index 62059de37..778183dab 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..4b644218a 100644
--- a/spec/memw.typ
+++ b/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)
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<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)
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<sign; X, signed>"))
 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]]