spec: Allow for cross referencing between different chapters, both in pdf and web mode

spec/add.typ

@@ -2,11 +2,11 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": render_chip_column_table, render_chip_assumptions, render_constraint_table
 
-#show: book-page.with(title: "ADD/SUB")
-
 #let config = load_config()
 #let chip = load_chip("src/add.toml", config)
 
+#show: book-page(chip.name)
+
 #let add = raw(chip.name)
 
 #let highlighted_code(code) = {
@@ -18,7 +18,6 @@
     raw(code))
 }
 
-= #add template
 #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

spec/bitwise.typ

@@ -13,9 +13,7 @@
 
 #let bitwise = raw(chip.name)
 
-#show: book-page.with(title: "BRANCH chip")
-
-= #bitwise chip
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/book.typ

@@ -1,31 +1,35 @@
 #import "@preview/shiroa:0.3.1": *
+#import "/templates/page.typ": project
 
 #show: book
 
-#book-meta(
+#let meta = (
   title: "Lambda VM specification",
-  summary: [
-    #chapter("memory.typ")[Memory argument]
-    #chapter("variables.typ")[Variables]
-    #chapter("is_bit.typ")[IS_BIT template]
-    #chapter("add.typ")[ADD template]
-    #chapter("decode.typ")[DECODE chip]
-    #chapter("cpu.typ")[CPU chip]
-    #chapter("shift.typ")[SHIFT chip]
-    #chapter("branch.typ")[BRANCH]
-    #chapter("memw.typ")[MEMW]
-    #chapter("lt.typ")[LT]
-    #chapter("mul.typ")[MUL chip]
-    #chapter("dvrm.typ")[DVRM chip]
-    #chapter("load.typ")[LOAD chip]
-    #chapter("ecall.typ")[ECALL chips]
-    #chapter("bitwise.typ")[BITWISE]
-  ]
+  authors: ("3MI Labs", "Aligned"),
+  summary: (
+    ("memory.typ", [Memory argument], <memory>),
+    ("variables.typ", [Variables], <vars>),
+    ("is_bit.typ", [IS_BIT template], <isbit>),
+    ("add.typ", [ADD/SUB template], <add>),
+    ("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>),
+  )
+)
+#book-meta(
+  title: meta.title,
+  authors: meta.authors,
+  summary: meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join()
 )
 
-// re-export page template
-#import "/templates/page.typ": project
-#let book-page = project
 
 #let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[
   #set text(fill: foreground)
@@ -47,3 +51,103 @@
            align(center, strong(text(fill: black, title))))
     #align(left, body)
 ])
+
+
+#let is-shiroa = "x-target" in sys.inputs
+
+// Strip styling to keep only "pure" content.
+// This is useful to avoid errors on the `set document(...)` in `project`
+// when invisibly including other chapters to resolve xrefs.
+#let strip-all(content) = {
+  if repr(content.func()) == "sequence" {
+    for c in content.children {
+      strip-all(c)
+    }
+  } else if repr(content.func()) == "styled" {
+    strip-all(content.child)
+  } else {
+    content
+  }
+}
+
+#let _toplevel = state("_toplevel", none)
+#let _xref-included = state("_xref-included", (:))
+
+// 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 _xref-included.update(x => x + ((f): true))
+}
+
+// Generate a cross-link for references to other chapters.
+// Leaves the ref untouched if it can't be resolved or points to the current chapter.
+#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)))
+  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)])
+    } else {
+      // Because shiroa does weird url escaping
+      let shiroa-label = label(str(lbl).replace(":", "%3A"))
+      xref-include(ch)
+      // 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
+      // when clicking.
+      // There may still be some way around it by messing with some html output
+      let link-content = context {
+        let fig = query(lbl).first()
+        let counter = if fig.has("counter") {
+          fig.counter
+        } else {
+          counter(fig.func())
+        }
+
+        let supplement = if rf.supplement == auto {
+          fig.fields().at("supplement", default: none)
+        } else {
+          rf.supplement
+        }
+        [#supplement#numbering(fig.numbering, ..counter.at(lbl))]
+      }
+      cross-link("/" + ch, reference: shiroa-label, link-content)
+    }
+  } else {
+    rf
+  }
+}
+
+#let book-page(file, ..args) = {
+  let file = if file.ends-with(".typ") {
+    file
+  } else {
+    lower(file) + ".typ"
+  }
+  assert(meta.summary.find(((f, _, _)) => f == file) != none, message: "Couldn't resolve typst source file " + file)
+  if is-shiroa {
+    (body) => {
+      context _xref-included.update(x => x + ((file): true))
+      context _toplevel.update(s => {
+        if s == none {
+          file
+        } else {
+          s
+        }
+      })
+      let cond() = _toplevel.final() == file
+      project.with(..args, title: context meta.summary.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([
+        #show ref: it => context if _toplevel.final() == file {
+          xref(it)
+        }
+        #body
+      ])
+    }
+  } else {
+    (body) => body
+  }
+}

spec/branch.typ

@@ -12,7 +12,7 @@
 #let config = load_config()
 #let chip = load_chip("src/branch.toml", config)
 
-#show: book-page.with(title: "BRANCH chip")
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/cpu.typ

@@ -12,7 +12,7 @@
 #let config = load_config()
 #let chip = load_chip("src/cpu.toml", config)
 
-#show: book-page.with(title: "CPU chip")
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/decode.typ

@@ -1,4 +1,4 @@
-#import "/book.typ": book-page, rj
+#import "/book.typ": book-page, rj, xref
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
@@ -11,11 +11,10 @@
 
 #let config = load_config()
 #let chip = load_chip("src/decode.toml", config)
-#show: book-page.with(title: "DECODE chip")
+#show: book-page(chip.name)
 
 #let decode = raw(chip.name)
 
-= #decode table
 All `RV64IMC` instruction are to be decoded to a format that can be interpreted by the VM.
 This section outlines the decoding table being used in the VM.
 For reasons of efficiency, data in this table is significantly compressed.
@@ -223,4 +222,4 @@ In addition to decoding all instructions provided in the ELF and adding a corres
 Note that this will never conflict with any entry in the ELF, since it has an odd `pc` value.
 
 This entry is used to pad the `CPU` table.
-More details on this matter are provided in the `CPU` chip.
+More details on this matter are provided in the `CPU` chip.

spec/dvrm.typ

@@ -12,6 +12,6 @@
 #let config = load_config()
 // #let chip = load_chip("src/dvrm.toml", config)
 
-#show: book-page.with(title: "DVRM chip")
+#show: book-page("dvrm.typ")
 
 *placeholder chapter: WIP*

spec/ebook.typ

@@ -1,12 +1,19 @@
-#import "@preview/shiroa:0.3.1": *
-#import "/book.typ": style
+#import "/book.typ": style, meta
 
-#import "/templates/ebook.typ"
+#set document(author: meta.authors, title: meta.title)
 
-#show: ebook.project.with(title: "typst-book", spec: "book.typ")
 #style.update((
   foreground: black,
 ))
 
-// set a resolver for inclusion
-#ebook.resolve-inclusion(it => include it)
+#align(center, title(meta.title))
+#pagebreak(weak: true)
+#outline()
+
+#show heading: set heading(numbering: "1.1")
+
+#meta.summary.map(((ch, title, ref)) => [
+  #pagebreak(weak: true)
+  #heading(supplement: [Chapter], level: 1, title)#ref
+  #include ch
+]).join()

spec/ecall.typ

@@ -11,7 +11,7 @@
 
 #let config = load_config()
 
-#show: book-page.with(title: "ECALL chips")
+#show: book-page("ecall.typ")
 
 *placeholder chapter: WIP*
 

spec/is_bit.typ

@@ -2,11 +2,11 @@
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": render_chip_column_table, render_constraint_table
 
-#show: book-page.with(title: "IS_BIT template")
-
 #let config = load_config()
 #let chip = load_chip("src/is_bit.toml", config)
 
+#show: book-page(chip.name)
+
 #let is_bit = raw(chip.name)
 
 #let highlighted_code(code) = {
@@ -18,7 +18,6 @@
     raw(code))
 }
 
-= #is_bit template
 #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.
 

spec/load.typ

@@ -12,7 +12,7 @@
 #let config = load_config()
 #let chip = load_chip("src/load.toml", config)
 
-#show: book-page.with(title: "LOAD chip")
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/lt.typ

@@ -12,7 +12,7 @@
 #let config = load_config()
 #let chip = load_chip("src/lt.toml", config)
 
-#show: book-page.with(title: "LT chip")
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/memory.typ

@@ -1,4 +1,4 @@
-#import "/book.typ": book-page, rj, aside
+#import "/book.typ": book-page, rj, aside, xref
 #import "/src.typ": load_config, load_chip
 #import "/chip.typ": (
   render_chip_assumptions,
@@ -12,9 +12,7 @@
 #let config = load_config()
 #let chip = load_chip("src/page.toml", config)
 
-#show: book-page.with(title: "Memory argument")
-
-= Memory argument
+#show: book-page("memory.typ")
 
 As part of fully proving the correct execution of a RISC-V program,
 the VM must ensure that memory reads and writes are consistent.
@@ -108,7 +106,7 @@ to have a strictly greater timestamp than the consumed token.
 This raises the question of how to represent timestamps and cleanly perform this check,
 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 functionality for comparisons.
+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]
 
 #aside[Note on options and trade-offs for timestamp representation][

spec/memw.typ

@@ -11,7 +11,7 @@
 #let config = load_config()
 #let chip = load_chip("src/memw.toml", config)
 
-#show: book-page.with(title: "MEMW chip")
+#show: book-page(chip.name)
 
 == Columns
 #let nr_variables = total_nr_variables(chip)

spec/mul.typ

@@ -12,12 +12,10 @@
 #let config = load_config()
 #let chip = load_chip("src/mul.toml", config)
 
-#show: book-page.with(title: "MUL chip")
+#show: book-page(chip.name)
 
 #let mul = raw(chip.name)
 
-= #mul chip
-
 == Columns
 #let nr_variables = total_nr_variables(chip)
 #let nr_columns = total_nr_instantiated_columns(chip, config)

spec/shift.typ

@@ -14,9 +14,7 @@
 
 #let shift = raw(chip.name)
 
-#show: book-page.with(title: "SHIFT chip")
-
-= #shift chip
+#show: book-page(chip.name)
 
 == Interface
 The #shift chip has the following interface: