spec: update TOC

spec/about_ecalls.typ

@@ -0,0 +1,24 @@
+#import "/book.typ": book-page, aside
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_column_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  render_constraint_table,
+  render_chip_assumptions,
+  render_chip_padding_table,
+)
+
+#let config = load_config()
+
+#show: book-page("about_ecalls.typ")
+
+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]]]),
+- the arguments are located in registers `A0`-`A6`, and
+- the return value is written to `A0`,
+where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
+#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]).

spec/book.typ

@@ -8,31 +8,53 @@
   authors: ("3MI Labs", "Aligned"),
   version: "0.2",
   summary: (
-    ("logup.typ", [LogUp argument], <logup>),
-    ("memory.typ", [Memory argument], <memory>),
-    ("variables.typ", [Variables], <vars>),
-    ("signatures.typ", [Signatures], <signatures>),
-    ("is_bit.typ", [IS_BIT template], <isbit>),
-    ("sign.typ", [SIGN template], <sign>),
-    ("add.typ", [ADD/SUB template], <add>),
-    ("neg.typ", [NEG template], <neg>),
-    ("decode.typ", [DECODE table], <decode>),
-    ("cpu.typ", [CPU chip], <cpu>),
-    ("shift.typ", [SHIFT chip], <shift>),
-    ("branch.typ", [BRANCH chip], <branch>),
-    ("memw.typ", [MEMW chip], <memw>),
-    ("lt.typ", [LT chip], <lt>),
-    ("mul.typ", [MUL chip], <mul>),
-    ("dvrm.typ", [DVRM chip], <dvrm>),
-    ("load.typ", [LOAD chip], <load>),
-    ("ecall.typ", [ECALL chips], <ecall>),
-    ("bitwise.typ", [BITWISE chips], <bitwise>),
+    ("PROOF SYSTEM", (
+        ("logup.typ", [LogUp argument], <logup>),
+        ("memory.typ", [Memory argument], <memory>),
+    )),
+    ("OVERVIEW", (
+        ("variables.typ", [Variables], <vars>),
+        ("signatures.typ", [Signatures], <signatures>),
+    )),
+    ("TEMPLATES", (
+      ("is_bit.typ", [IS_BIT template], <isbit>),
+      ("sign.typ", [SIGN template], <sign>),
+      ("add.typ", [ADD/SUB template], <add>),
+      ("neg.typ", [NEG template], <neg>),
+    )),
+    ("MEMORY", (
+      ("memw.typ", [MEMW chip], <memw>),
+    )),
+    ("CPU", (
+      ("decode.typ", [DECODE table], <decode>),
+      ("cpu.typ", [CPU chip], <cpu>),
+    )),
+    ("ALU", (
+      ("shift.typ", [SHIFT chip], <shift>),
+      ("branch.typ", [BRANCH chip], <branch>),
+      ("lt.typ", [LT chip], <lt>),
+      ("mul.typ", [MUL chip], <mul>),
+      ("dvrm.typ", [DVRM chip], <dvrm>),
+      ("load.typ", [LOAD chip], <load>),
+      ("bitwise.typ", [BITWISE chips], <bitwise>),
+    )),
+    ("ECALLS", (
+      ("about_ecalls.typ", [About ECALL], <ecall>),
+      ("halt.typ", [HALT chip], <halt>),
+      ("commit.typ", [COMMIT chip], <commit>),
+    ))
   )
 )
+#let meta_sections = meta.summary.map(m => m.at(1)).sum()
 #book-meta(
   title: meta.title,
   authors: meta.authors,
-  summary: prefix-chapter("front.typ", meta.title) + meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join()
+  summary: prefix-chapter("front.typ", meta.title) 
+    + meta.summary.map(
+      ((title, sections)) => {
+        heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join()
+      }
+    ).join()
 )
 
 #let common-formatting(body) = {
@@ -93,11 +115,11 @@
 #let xref(rf) = {
   assert(is-shiroa, message: "xref should only be used when compiling for shiroa")
   let lbl = rf.target
-  let found = meta.summary.find(((_, _, tag)) => str(lbl).starts-with(str(tag)))
+  let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag)))
   context if found != none and found.at(0) != _toplevel.final() {
     let (ch, title, ref) = found
     if ref == lbl {
-      cross-link("/" + ch, [Chapter #(meta.summary.position(x => x == found) + 1)])
+      cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)])
     } else {
       // Because shiroa does weird url escaping
       let shiroa-label = label(str(lbl).replace(":", "%3A"))
@@ -130,12 +152,12 @@
 }
 
 #let book-page(file, ..args) = {
-  let file = if file.ends-with(".typ") {
-    file
-  } else {
-    lower(file) + ".typ"
+  if not file.ends-with(".typ") {
+    file = lower(file) + ".typ"
   }
-  assert(meta.summary.find(((f, _, _)) => f == file) != none, message: "Couldn't resolve typst source file " + file)
+
+  assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file)
+
   if is-shiroa {
     (body) => {
       show: common-formatting
@@ -147,7 +169,7 @@
         }
       })
       let cond() = _toplevel.final() == file
-      project.with(..args, title: context meta.summary.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([
+      project.with(..args, title: context meta_sections.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([
         #show ref: it => context if _toplevel.final() == file {
           xref(it)
         }

spec/ecall.typ → spec/commit.typ

@@ -10,80 +10,21 @@
   render_chip_padding_table,
 )
 
-#let config = load_config()
-
-#show: book-page("ecall.typ")
-
-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]]]),
-- the arguments are located in registers `A0`-`A6`, and
-- the return value is written to `A0`,
-where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
-#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]).
-
-
-#let config = load_config()
-#let chip = load_chip("src/halt.toml", config)
-#let halt = raw(chip.name)
-= #halt chip
-
-== Columns
-#let nr_variables = total_nr_variables(chip)
-#let nr_columns = total_nr_instantiated_columns(chip, config)
-#let nr_halt_interactions = compute_nr_interactions(chip)
-
-The #halt chip leverages #nr_variables variable, spanning #nr_columns columns and leverages #nr_halt_interactions interaction(s):
-#render_chip_column_table(chip, config)
-
-== Assumptions
-It is assumed the input is range checked:
-#render_chip_assumptions(chip, config)
-
-== Constraints
-The #halt chip:
-+ makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code),
-+ writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and
-+ sets `pc` equal to $1$ (@halt:c:pc).
-Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp.
-This prevents any other operation involving memory from being executed hereafter.
-#render_constraint_table(chip, config, groups: "all")
-
-#aside("Note on register clean up",
-[
-  Observe that --- in its current state --- this solution puts the burden of verifying the register cleanup on the verifier inside of the lookup argument.
-  Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there.
-])
-
-=== Lookup
-In this VM, halting is considered equivalent to executing a `sys_exit`.
-Hence, this chip responds to `ECALL`s with system call number 93.
-#footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L258")[[src]]])
-The HALT chip therefore contributes the following interaction to the lookup-argument:
-#render_constraint_table(chip, config, groups: "lookup")
-
-== Padding
-This chip should only contain a single row.
-Given that $2^0 = 1$, this chip does not need to be padded.
-As such, no padding is defined.
-
+#show: book-page("commit.typ")
 
 #let config = load_config()
 #let chip = load_chip("src/commit.toml", config)
 #let commit = raw(chip.name)
-= #commit chip
 
-== Columns
+= Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)
-#let nr_commit_interactions = compute_nr_interactions(chip)
+#let nr_interactions = compute_nr_interactions(chip)
 
-The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_commit_interactions interactions:
+The #commit chip leverages #nr_variables variables, spanning #nr_columns columns and leverages #nr_interactions interactions:
 #render_chip_column_table(chip, config)
 
-== Constraints
+= Constraints
 In this VM, committing is considered equivalent to writing a value to `stdout`.
 Hence, this chip responds to `ECALL`s with system call number 64.
 #footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L174")[[src]]])
@@ -152,11 +93,11 @@ Lastly, we must make sure `first`, `end` and `μ` are bits (@commit:c:range_firs
 These are required to ensure the multiplicities $-(#`μ` - #`first`)$ and $#`μ` - #`end`$ are binary.
 #render_constraint_table(chip, config, groups: "bits")
 
-== Padding
+= Padding
 To pad this chip, use the below data.
 #render_chip_padding_table(chip, config)
 
-== Notes/optimizations
+= Notes/optimizations
 - The current version only supports writing to `stdout`.
   This chip could potentially be extended to support writing to arbitrary `fd`s
 - One might be able to replace @commit:c:end by `end => count = 0`.

spec/ebook.typ

@@ -6,15 +6,39 @@
 #align(center, text(style: "italic", fill: luma(40%))[Version #meta.version])
 #align(center, meta.authors.join(", "))
 #pagebreak(weak: true)
-#outline()
+
+// outline
+#show outline.entry.where(level: 1): set outline.entry(fill: line(length: 100%, stroke: stroke(dash: "solid")))
+#show outline.entry.where(level: 1): it => {
+  v(15pt, weak: true)
+  strong(it)
+  v(5pt, weak: true)
+}
+#show outline.entry.where(level: 2): it => {
+  v(10pt, weak: true)
+  it
+}
+#outline(depth: 3)
+
+// chapter pages
+#show heading.where(level: 1): it => align(center + horizon)[#underline(it, offset: 10pt, extent: 5pt)]
 
 #show: common-formatting
-#show heading: set heading(numbering: "1.1")
+#show heading: set heading(numbering: (..args) => {
+    let args = args.pos()
+    let skip_first = args.slice(calc.min(args.len(), 1))
+    numbering("1.1", ..skip_first)
+})
 #show raw.where(block: true): set block(fill: luma(230))
 
-#meta.summary.map(((ch, title, ref)) => [
-  #pagebreak(weak: true)
-  #heading(supplement: [Chapter], level: 1, title)#ref
-  #set heading(offset: 1)
-  #include ch
-]).join()
+#for (ch_title, sections) in meta.summary {
+  pagebreak(weak: true)
+  heading(supplement: [Chapter], level: 1, ch_title, numbering: none)
+
+  for (sec, sec_title, ref) in sections {
+    pagebreak(weak: true)
+    [#heading(level: 2, supplement: [Section], sec_title)#ref]
+    set heading(offset: 2)
+    include sec
+  }
+}

spec/halt.typ

@@ -0,0 +1,56 @@
+#import "/book.typ": book-page, aside
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_column_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  compute_nr_interactions,
+  render_constraint_table,
+  render_chip_assumptions,
+  render_chip_padding_table,
+)
+
+#show: book-page("halt.typ")
+
+#let config = load_config()
+#let chip = load_chip("src/halt.toml", config)
+#let halt = raw(chip.name)
+
+= Columns
+#let nr_variables = total_nr_variables(chip)
+#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)
+
+= Assumptions
+It is assumed the input is range checked:
+#render_chip_assumptions(chip, config)
+
+= Constraints
+The #halt chip:
++ makes sure register `x10` (containing the exit code) equals $0$ (@halt:c:read_zero_exit_code),
++ writes $0$ to all other registers (@halt:c:zeroize_registers_lo/@halt:c:zeroize_registers_hi), and
++ sets `pc` equal to $1$ (@halt:c:pc).
+Note that the writes performed by all these interactions are accompanied by the timestamp $2^64-1$; the maximum timestamp.
+This prevents any other operation involving memory from being executed hereafter.
+#render_constraint_table(chip, config, groups: "all")
+
+#aside("Note on register clean up",
+[
+  Observe that --- in its current state --- this solution puts the burden of verifying the register cleanup on the verifier inside of the lookup argument.
+  Alternatively, one could add 31 lookups to the "memory" table to remove the _known_ final tokens for the registers there.
+])
+
+== Lookup
+In this VM, halting is considered equivalent to executing a `sys_exit`.
+Hence, this chip responds to `ECALL`s with system call number 93.
+#footnote([RISC-V GNU-toolchain, `unistd.h`; version 2026-01-23, #link("https://github.com/riscv-collab/riscv-gnu-toolchain/blob/2026.01.23/linux-headers/include/asm-generic/unistd.h#L258")[[src]]])
+The HALT chip therefore contributes the following interaction to the lookup-argument:
+#render_constraint_table(chip, config, groups: "lookup")
+
+= Padding
+This chip should only contain a single row.
+Given that $2^0 = 1$, this chip does not need to be padded.
+As such, no padding is defined.