From 87e9b87a7bb6e946210dfd117884ea6c2942ed86 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 23 Jan 2026 17:39:58 +0100 Subject: [PATCH 1/9] spec: Allow for cross referencing between different chapters, both in pdf and web mode --- spec/book.typ | 43 +++++++++++++++++++++++++++++++++++++++++++ spec/decode.typ | 6 +++--- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index 29e61350c..5f5b251ea 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -47,3 +47,46 @@ align(center, strong(text(fill: black, title)))) #align(left, body) ]) + +#let is-shiroa = is-web-target() + +#show figure: repr + +#let _xref-included = state("_xref-included", (:)) + +#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 xref(file, lbl, ..ref-args) = { + if is-shiroa { + // Because shiroa does weird url escaping + let shiroa-label = label(str(lbl).replace(":", "%3A")) + context if file not in _xref-included.get() { + // Let's blow up the compile times :) + hide(box(width: 0%, height: 0%, strip-all(include file))) + _xref-included.update(it => it + ((file): true)) + } + let link-content = context { + let fig = query(lbl).first() + let counter = if fig.has("counter") { + fig.counter + } else { + counter(fig.func()) + } + + [#ref-args.named().at("supplement", default: [])#numbering(fig.numbering, ..counter.at(lbl))] + } + cross-link(file, reference: shiroa-label, link-content) + } else { + ref(lbl, ..ref-args) + } +} diff --git a/spec/decode.typ b/spec/decode.typ index d8332e033..c5ee18e77 100644 --- a/spec/decode.typ +++ b/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, @@ -36,7 +36,7 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this "padding-instruction" would immediately make the CPU table unprovable. +Given that `CPU` asserts that `EBREAK = 0` (see #xref("/cpu.typ", )), using this "padding-instruction" would immediately make the CPU table unprovable. Note moreover that the `pc` is set to $7$. This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). @@ -223,4 +223,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. \ No newline at end of file +More details on this matter are provided in the `CPU` chip. From 5a843a95ca3ed1c6199708e097f95950afe5f8db Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 26 Jan 2026 13:26:20 +0100 Subject: [PATCH 2/9] Improve PDF organization The PDF now no longer depends on shiroa trickery to compile, so errors are more clearly visible instead of being hidden behind layour iterations. Additionally, we can now have nice chapter headings and references to them. --- spec/add.typ | 3 +- spec/bitwise.typ | 4 +- spec/book.typ | 85 +++++++++++++++++++++++----------------- spec/branch.typ | 2 +- spec/cpu.typ | 2 +- spec/decode.typ | 5 +-- spec/dvrm.typ | 2 +- spec/ebook.typ | 16 +++++--- spec/ecall.typ | 2 +- spec/is_bit.typ | 3 +- spec/load.typ | 2 +- spec/lt.typ | 2 +- spec/memory.typ | 8 ++-- spec/memw.typ | 2 +- spec/mul.typ | 4 +- spec/shift.typ | 4 +- spec/templates/ebook.typ | 37 ----------------- spec/variables.typ | 3 +- 18 files changed, 78 insertions(+), 108 deletions(-) delete mode 100644 spec/templates/ebook.typ diff --git a/spec/add.typ b/spec/add.typ index 0dade7b01..e18826e3c 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -2,7 +2,7 @@ #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") +#show: book-page("add.typ") #let config = load_config() #let chip = load_chip("src/add.toml", config) @@ -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 diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 34ec6dd10..ef8db56f3 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -13,9 +13,7 @@ #let bitwise = raw(chip.name) -#show: book-page.with(title: "BRANCH chip") - -= #bitwise chip +#show: book-page("bitwise.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/book.typ b/spec/book.typ index 5f5b251ea..88da8bb97 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -2,30 +2,41 @@ #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]), + ("variables.typ", [Variables]), + ("is_bit.typ", [IS_BIT template]), + ("add.typ", [ADD/SUB template]), + ("decode.typ", [DECODE table]), + ("cpu.typ", [CPU chip]), + ("shift.typ", [SHIFT chip]), + ("branch.typ", [BRANCH chip]), + ("memw.typ", [MEMW chip]), + ("lt.typ", [LT chip]), + ("mul.typ", [MUL chip]), + ("dvrm.typ", [DVRM chip]), + ("load.typ", [LOAD chip]), + ("ecall.typ", [ECALL chips]), + ("bitwise.typ", [BITWISE chips]), + ) +) +#book-meta( + title: meta.title, + authors: meta.authors, + summary: meta.summary.map(((ch, title)) => chapter(ch, title)).join() ) -// re-export page template +#let is-shiroa = "x-target" in sys.inputs + #import "/templates/page.typ": project -#let book-page = project +#let book-page(file, ..args) = if is-shiroa { + (body) => project.with(..args, title: meta.summary.find(((ch, title)) => ch == file).at(1))(body) +} else { + (body) => body +} #let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[ #set text(fill: foreground) @@ -48,8 +59,6 @@ #align(left, body) ]) -#let is-shiroa = is-web-target() - #show figure: repr #let _xref-included = state("_xref-included", (:)) @@ -66,27 +75,31 @@ } } -#let xref(file, lbl, ..ref-args) = { +#let xref(file, lbl: none, ..ref-args) = { if is-shiroa { - // Because shiroa does weird url escaping - let shiroa-label = label(str(lbl).replace(":", "%3A")) - context if file not in _xref-included.get() { + if lbl == none { + cross-link(file, [Chapter #(meta.summary.position(((ch, title)) => "/"+ch == file) + 1)]) + } else { + // Because shiroa does weird url escaping + let shiroa-label = label(str(lbl).replace(":", "%3A")) + context if file not in _xref-included.get() { // Let's blow up the compile times :) hide(box(width: 0%, height: 0%, strip-all(include file))) _xref-included.update(it => it + ((file): true)) - } - let link-content = context { - let fig = query(lbl).first() - let counter = if fig.has("counter") { - fig.counter - } else { - counter(fig.func()) } + let link-content = context { + let fig = query(lbl).first() + let counter = if fig.has("counter") { + fig.counter + } else { + counter(fig.func()) + } - [#ref-args.named().at("supplement", default: [])#numbering(fig.numbering, ..counter.at(lbl))] + [#ref-args.named().at("supplement", default: [])#numbering(fig.numbering, ..counter.at(lbl))] + } + cross-link(file, reference: shiroa-label, link-content) } - cross-link(file, reference: shiroa-label, link-content) } else { - ref(lbl, ..ref-args) + ref(if lbl != none { lbl } else { label(file) }, ..ref-args) } } diff --git a/spec/branch.typ b/spec/branch.typ index a18c252b7..08eb9ccc9 100644 --- a/spec/branch.typ +++ b/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("branch.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/cpu.typ b/spec/cpu.typ index 784d750d2..566bdd794 100644 --- a/spec/cpu.typ +++ b/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("cpu.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/decode.typ b/spec/decode.typ index c5ee18e77..f031ca575 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -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("decode.typ") #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. @@ -36,7 +35,7 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0` (see #xref("/cpu.typ", )), using this "padding-instruction" would immediately make the CPU table unprovable. +Given that `CPU` asserts that `EBREAK = 0` (see #xref("/cpu.typ", lbl: )), using this "padding-instruction" would immediately make the CPU table unprovable. Note moreover that the `pc` is set to $7$. This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). diff --git a/spec/dvrm.typ b/spec/dvrm.typ index 69e79cee2..f1d9a3a4c 100644 --- a/spec/dvrm.typ +++ b/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* diff --git a/spec/ebook.typ b/spec/ebook.typ index 410e926bb..efcb3a78f 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -1,12 +1,18 @@ #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 heading: set heading(numbering: "1.1") -#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)) +// #outline() + +#meta.summary.map(((ch, title)) => [ + #heading(supplement: [Chapter], level: 1, title)#label("/"+ch) + #include ch +]).join() diff --git a/spec/ecall.typ b/spec/ecall.typ index fee25768c..3bf2d3b69 100644 --- a/spec/ecall.typ +++ b/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* diff --git a/spec/is_bit.typ b/spec/is_bit.typ index c379080cd..8afd4d69b 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -2,7 +2,7 @@ #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") +#show: book-page("is_bit.typ") #let config = load_config() #let chip = load_chip("src/is_bit.toml", config) @@ -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. diff --git a/spec/load.typ b/spec/load.typ index 931611108..25144a037 100644 --- a/spec/load.typ +++ b/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("load.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/lt.typ b/spec/lt.typ index 3b57a62e3..aecc93f41 100644 --- a/spec/lt.typ +++ b/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("lt.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/memory.typ b/spec/memory.typ index 6687d733d..a6bc0769b 100644 --- a/spec/memory.typ +++ b/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") // TODO: can we get rid of this? 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 (#xref("/lt.typ")) functionality for comparisons. #rj[Properly link/refer to the LT chip] #aside[Note on options and trade-offs for timestamp representation][ diff --git a/spec/memw.typ b/spec/memw.typ index bcf6a64b0..29f183ced 100644 --- a/spec/memw.typ +++ b/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("memw.typ") == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/mul.typ b/spec/mul.typ index 1892994f0..a2d231f6f 100644 --- a/spec/mul.typ +++ b/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("mul.typ") #let mul = raw(chip.name) -= #mul chip - == Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) diff --git a/spec/shift.typ b/spec/shift.typ index 70aebc97c..07def2327 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -14,9 +14,7 @@ #let shift = raw(chip.name) -#show: book-page.with(title: "SHIFT chip") - -= #shift chip +#show: book-page("shift.typ") == Interface The #shift chip has the following interface: diff --git a/spec/templates/ebook.typ b/spec/templates/ebook.typ deleted file mode 100644 index 44e0312d3..000000000 --- a/spec/templates/ebook.typ +++ /dev/null @@ -1,37 +0,0 @@ -#import "@preview/shiroa:0.3.1": * -#import "/templates/page.typ": part-style, project - -#let _page-project = project - -#let _resolve-inclusion-state = state("_resolve-inclusion", none) - -#let resolve-inclusion(inc) = _resolve-inclusion-state.update(it => inc) - -#let project(title: "", authors: (), spec: "", content) = { - // Set document metadata early - set document( - author: authors, - title: title, - ) - - // Inherit from gh-pages - show: _page-project - - if title != "" { - heading(title) - } - - context { - let inc = _resolve-inclusion-state.final() - external-book(spec: inc(spec)) - - let mt = book-meta-state.final() - let styles = (inc: inc, part: part-style, chapter: it => it) - - if mt != none { - mt.summary.map(it => visit-summary(it, styles)).sum() - } - } - - content -} diff --git a/spec/variables.typ b/spec/variables.typ index 42e7bc379..d62fec7ac 100644 --- a/spec/variables.typ +++ b/spec/variables.typ @@ -1,11 +1,10 @@ #import "/book.typ": book-page #import "/src.typ": load_config -#show: book-page.with(title: "Variables") +#show: book-page("variables.typ") #let config = load_config() -= Variables While this VM operates on 64-bit words, the proving system's base field has fewer than $2^64$ elements available and thus cannot represent all words natively. To this end, we introduce the concept of "variables" as an abstraction layer on top of the VM's field elements. The following table lists all variable types used in this VM. From dd520008ad52502068b7c75a6c35a40f5a8d2259 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 26 Jan 2026 13:52:51 +0100 Subject: [PATCH 3/9] Allow xref by specifying only the label --- spec/book.typ | 53 +++++++++++++++++++++++++------------------------ spec/decode.typ | 2 +- spec/ebook.typ | 4 ++-- spec/memory.typ | 2 +- 4 files changed, 31 insertions(+), 30 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index 88da8bb97..6bb492a0c 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -6,34 +6,34 @@ title: "Lambda VM specification", authors: ("3MI Labs", "Aligned"), summary: ( - ("memory.typ", [Memory argument]), - ("variables.typ", [Variables]), - ("is_bit.typ", [IS_BIT template]), - ("add.typ", [ADD/SUB template]), - ("decode.typ", [DECODE table]), - ("cpu.typ", [CPU chip]), - ("shift.typ", [SHIFT chip]), - ("branch.typ", [BRANCH chip]), - ("memw.typ", [MEMW chip]), - ("lt.typ", [LT chip]), - ("mul.typ", [MUL chip]), - ("dvrm.typ", [DVRM chip]), - ("load.typ", [LOAD chip]), - ("ecall.typ", [ECALL chips]), - ("bitwise.typ", [BITWISE chips]), + ("memory.typ", [Memory argument], ), + ("variables.typ", [Variables], ), + ("is_bit.typ", [IS_BIT template], ), + ("add.typ", [ADD/SUB template], ), + ("decode.typ", [DECODE table], ), + ("cpu.typ", [CPU chip], ), + ("shift.typ", [SHIFT chip], ), + ("branch.typ", [BRANCH chip], ), + ("memw.typ", [MEMW chip], ), + ("lt.typ", [LT chip], ), + ("mul.typ", [MUL chip], ), + ("dvrm.typ", [DVRM chip], ), + ("load.typ", [LOAD chip], ), + ("ecall.typ", [ECALL chips], ), + ("bitwise.typ", [BITWISE chips], ), ) ) #book-meta( title: meta.title, authors: meta.authors, - summary: meta.summary.map(((ch, title)) => chapter(ch, title)).join() + summary: meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join() ) #let is-shiroa = "x-target" in sys.inputs #import "/templates/page.typ": project #let book-page(file, ..args) = if is-shiroa { - (body) => project.with(..args, title: meta.summary.find(((ch, title)) => ch == file).at(1))(body) + (body) => project.with(..args, title: meta.summary.find(x => x.at(0) == file).at(1))(body) } else { (body) => body } @@ -75,17 +75,18 @@ } } -#let xref(file, lbl: none, ..ref-args) = { +#let xref(lbl, ..ref-args) = { if is-shiroa { - if lbl == none { - cross-link(file, [Chapter #(meta.summary.position(((ch, title)) => "/"+ch == file) + 1)]) + let found = meta.summary.find(x => str(lbl).starts-with(str(x.at(2)))) + 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")) - context if file not in _xref-included.get() { - // Let's blow up the compile times :) - hide(box(width: 0%, height: 0%, strip-all(include file))) - _xref-included.update(it => it + ((file): true)) + context if ch not in _xref-included.get() { + hide(box(width: 0%, height: 0%, strip-all(include "/" + ch))) + _xref-included.update(it => it + ((ch): true)) } let link-content = context { let fig = query(lbl).first() @@ -97,9 +98,9 @@ [#ref-args.named().at("supplement", default: [])#numbering(fig.numbering, ..counter.at(lbl))] } - cross-link(file, reference: shiroa-label, link-content) + cross-link("/" + ch, reference: shiroa-label, link-content) } } else { - ref(if lbl != none { lbl } else { label(file) }, ..ref-args) + ref(lbl) } } diff --git a/spec/decode.typ b/spec/decode.typ index f031ca575..45e535298 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -35,7 +35,7 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0` (see #xref("/cpu.typ", lbl: )), using this "padding-instruction" would immediately make the CPU table unprovable. +Given that `CPU` asserts that `EBREAK = 0` (see #xref()), using this "padding-instruction" would immediately make the CPU table unprovable. Note moreover that the `pc` is set to $7$. This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). diff --git a/spec/ebook.typ b/spec/ebook.typ index efcb3a78f..083097c9c 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -12,7 +12,7 @@ #align(center, title(meta.title)) // #outline() -#meta.summary.map(((ch, title)) => [ - #heading(supplement: [Chapter], level: 1, title)#label("/"+ch) +#meta.summary.map(((ch, title, ref)) => [ + #heading(supplement: [Chapter], level: 1, title)#ref #include ch ]).join() diff --git a/spec/memory.typ b/spec/memory.typ index a6bc0769b..3dcea512a 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -106,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 (#xref("/lt.typ")) functionality for comparisons. +We choose to represent timestamps as machine words, using the existing `LT` chip (#xref()) functionality for comparisons. #rj[Properly link/refer to the LT chip] #aside[Note on options and trade-offs for timestamp representation][ From ca9515a8cf0cf1dbfa3b27cdbb3115820c95eca7 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 26 Jan 2026 19:13:59 +0100 Subject: [PATCH 4/9] document strip-all --- spec/book.typ | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spec/book.typ b/spec/book.typ index 6bb492a0c..0094d4266 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -63,6 +63,9 @@ #let _xref-included = state("_xref-included", (:)) +// 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 { From db8b664c5ef5f1438ebf7fbe4ffda32fd256fb52 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 26 Jan 2026 23:00:40 +0100 Subject: [PATCH 5/9] It does work, after all; with only ~7GB of RAM usage for the entire thing --- spec/book.typ | 64 +++++++++++++++++++++++++++++------------ spec/decode.typ | 2 +- spec/memory.typ | 2 +- spec/templates/page.typ | 41 ++++++++++++++------------ 4 files changed, 70 insertions(+), 39 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index 0094d4266..a7d9c1e72 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -1,4 +1,5 @@ #import "@preview/shiroa:0.3.1": * +#import "/templates/page.typ": project #show: book @@ -31,13 +32,6 @@ #let is-shiroa = "x-target" in sys.inputs -#import "/templates/page.typ": project -#let book-page(file, ..args) = if is-shiroa { - (body) => project.with(..args, title: meta.summary.find(x => x.at(0) == file).at(1))(body) -} else { - (body) => body -} - #let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[ #set text(fill: foreground) *TODO #if name != none { [(#name)] }*: #body @@ -59,10 +53,6 @@ #align(left, body) ]) -#show figure: repr - -#let _xref-included = state("_xref-included", (:)) - // 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. @@ -78,19 +68,33 @@ } } -#let xref(lbl, ..ref-args) = { - if is-shiroa { - let found = meta.summary.find(x => str(lbl).starts-with(str(x.at(2)))) +#let _toplevel = state("_toplevel", none) +#let _xref-included = state("_xref-included", (:)) + +#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)) +} + +#let xref(rf, ..ref-args) = { + assert(is-shiroa, message: "xref should only be used when compiling for shiroa") + let lbl = rf.target + let found = meta.summary.find(x => str(lbl).starts-with(str(x.at(2)))) + 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")) - context if ch not in _xref-included.get() { - hide(box(width: 0%, height: 0%, strip-all(include "/" + ch))) - _xref-included.update(it => it + ((ch): true)) - } + 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") { @@ -104,6 +108,28 @@ cross-link("/" + ch, reference: shiroa-label, link-content) } } else { - ref(lbl) + rf + } +} + +#let book-page(file, ..args) = 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, description: "aaa", title: meta.summary.find(x => x.at(0) == file).at(1), cond: cond)([ + #show ref: it => context if _toplevel.final() == file { + xref(it) + } + #body + ]) } +} else { + (body) => body } diff --git a/spec/decode.typ b/spec/decode.typ index 45e535298..5abc443f7 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -35,7 +35,7 @@ Empty rows with the following content can be added to achieve this: #render_chip_padding_table(chip, config) Note that this row sets the `EBREAK` flag. -Given that `CPU` asserts that `EBREAK = 0` (see #xref()), using this "padding-instruction" would immediately make the CPU table unprovable. +Given that `CPU` asserts that `EBREAK = 0` (see @cpu:c:ebreak_traps), using this "padding-instruction" would immediately make the CPU table unprovable. Note moreover that the `pc` is set to $7$. This value is the _smallest odd number_ (i.e., not reachable during regular execution) that is more than _$4$_ (i.e., the max `pc`-increment) greater than _$1$_ (i.e., the `pc`-value used in the #link()[additional instruction] referred to by `CPU`-padding lines). diff --git a/spec/memory.typ b/spec/memory.typ index 3dcea512a..6d1baae41 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -106,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 (#xref()) 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][ diff --git a/spec/templates/page.typ b/spec/templates/page.typ index 1f7f88ea0..24d2c01f5 100644 --- a/spec/templates/page.typ +++ b/spec/templates/page.typ @@ -86,7 +86,7 @@ /// - authors (array | str): The author(s) of the page. /// - kind (str): The kind of the page. /// - plain-body (content): The plain body of the page. -#let project(title: "Typst Book", description: auto, authors: (), kind: "page", plain-body) = { +#let project(title: "Typst Book", description: auto, authors: (), kind: "page", cond: none, plain-body) = { // set basic document metadata set document( author: authors, @@ -137,23 +137,28 @@ lang: "en", ) - // markup setting - show: markup-rules.with( - ..common, - themes: themes, - heading-sizes: heading-sizes, - list-indent: list-indent, - main-size: main-size, - ) - // math setting - show: equation-rules.with(..common, theme-box: theme-box) - // code block setting - show: code-block-rules.with(..common, themes: themes, code-font: code-font) - - // Main body. - set par(justify: true) - - plain-body + context if cond() { + // markup setting + show: markup-rules.with( + ..common, + themes: themes, + heading-sizes: heading-sizes, + list-indent: list-indent, + main-size: main-size, + ) + + // math setting + show: equation-rules.with(..common, theme-box: theme-box) + // code block setting + show: code-block-rules.with(..common, themes: themes, code-font: code-font) + + // Main body. + set par(justify: true) + + plain-body + } else { + plain-body + } } #let part-style = heading From 91244b0b29f7954bedf47ef854901c9e9668b7e6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 11:00:23 +0100 Subject: [PATCH 6/9] small cleanup --- spec/book.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index a7d9c1e72..909bd8a4e 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -73,7 +73,7 @@ #let xref-include(f) = { context if f not in _xref-included.get() { - (hide(box(width: 0%, height: 0%, strip-all(include "/" + f)))) + hide(box(width: 0%, height: 0%, strip-all(include "/" + f))) } context _xref-included.update(x => x + ((f): true)) } @@ -123,7 +123,7 @@ } }) let cond() = _toplevel.final() == file - project.with(..args, description: "aaa", title: meta.summary.find(x => x.at(0) == file).at(1), cond: cond)([ + 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) } From 5f2f34edb32488f89c1f6990268d478a2232e76c Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 13:55:01 +0100 Subject: [PATCH 7/9] Update spec/book.typ Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/book.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/book.typ b/spec/book.typ index 909bd8a4e..7e1e67a2e 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -81,7 +81,7 @@ #let xref(rf, ..ref-args) = { assert(is-shiroa, message: "xref should only be used when compiling for shiroa") let lbl = rf.target - let found = meta.summary.find(x => str(lbl).starts-with(str(x.at(2)))) + 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 { From d234e5c71de35575d71fe878a844d8e78ff6e631 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 14:12:28 +0100 Subject: [PATCH 8/9] Address some review comments --- spec/book.typ | 16 +++++++++++++--- spec/ebook.typ | 9 +++++---- spec/templates/page.typ | 3 +++ 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/spec/book.typ b/spec/book.typ index 7e1e67a2e..5d9af0889 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -30,7 +30,6 @@ summary: meta.summary.map(((ch, title, _ref)) => chapter(ch, title)).join() ) -#let is-shiroa = "x-target" in sys.inputs #let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.5em, radius: 20%, stroke: black)[ #set text(fill: foreground) @@ -53,6 +52,9 @@ #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. @@ -71,6 +73,7 @@ #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))) @@ -78,7 +81,9 @@ context _xref-included.update(x => x + ((f): true)) } -#let xref(rf, ..ref-args) = { +// 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))) @@ -103,7 +108,12 @@ counter(fig.func()) } - [#ref-args.named().at("supplement", default: [])#numbering(fig.numbering, ..counter.at(lbl))] + 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) } diff --git a/spec/ebook.typ b/spec/ebook.typ index 083097c9c..835751163 100644 --- a/spec/ebook.typ +++ b/spec/ebook.typ @@ -1,18 +1,19 @@ -#import "@preview/shiroa:0.3.1": * #import "/book.typ": style, meta #set document(author: meta.authors, title: meta.title) -#show heading: set heading(numbering: "1.1") - #style.update(( foreground: black, )) #align(center, title(meta.title)) -// #outline() +#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() diff --git a/spec/templates/page.typ b/spec/templates/page.typ index 24d2c01f5..4ec7b27ac 100644 --- a/spec/templates/page.typ +++ b/spec/templates/page.typ @@ -85,6 +85,9 @@ /// - Hint: use `""` to generate an empty description. /// - authors (array | str): The author(s) of the page. /// - kind (str): The kind of the page. +/// - cond (function): A predicate that can be used inside of `context` +/// to check whether display rules should be applied. +/// Useful for including other chapters invisibly to figure out information about their labels /// - plain-body (content): The plain body of the page. #let project(title: "Typst Book", description: auto, authors: (), kind: "page", cond: none, plain-body) = { // set basic document metadata From f73dc28cc2d1fdce0f14834c59ee433900584428 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 27 Jan 2026 14:41:16 +0100 Subject: [PATCH 9/9] less repetition for file names --- spec/add.typ | 4 ++-- spec/bitwise.typ | 2 +- spec/book.typ | 46 +++++++++++++++++++++++++++------------------- spec/branch.typ | 2 +- spec/cpu.typ | 2 +- spec/decode.typ | 2 +- spec/is_bit.typ | 4 ++-- spec/load.typ | 2 +- spec/lt.typ | 2 +- spec/memory.typ | 2 +- spec/memw.typ | 2 +- spec/mul.typ | 2 +- spec/shift.typ | 2 +- 13 files changed, 41 insertions(+), 33 deletions(-) diff --git a/spec/add.typ b/spec/add.typ index e18826e3c..981a0ccb1 100644 --- a/spec/add.typ +++ b/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("add.typ") - #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) = { diff --git a/spec/bitwise.typ b/spec/bitwise.typ index ef8db56f3..9b5b4a638 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -13,7 +13,7 @@ #let bitwise = raw(chip.name) -#show: book-page("bitwise.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/book.typ b/spec/book.typ index 5d9af0889..b194b7f70 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -122,24 +122,32 @@ } } -#let book-page(file, ..args) = 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 - ]) +#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 } -} else { - (body) => body } diff --git a/spec/branch.typ b/spec/branch.typ index 08eb9ccc9..f448f2da4 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/branch.toml", config) -#show: book-page("branch.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/cpu.typ b/spec/cpu.typ index 566bdd794..0afa75f62 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/cpu.toml", config) -#show: book-page("cpu.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/decode.typ b/spec/decode.typ index 5abc443f7..c68b1ae53 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -11,7 +11,7 @@ #let config = load_config() #let chip = load_chip("src/decode.toml", config) -#show: book-page("decode.typ") +#show: book-page(chip.name) #let decode = raw(chip.name) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 8afd4d69b..a12d62108 100644 --- a/spec/is_bit.typ +++ b/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("is_bit.typ") - #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) = { diff --git a/spec/load.typ b/spec/load.typ index 25144a037..71c274d1b 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/load.toml", config) -#show: book-page("load.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/lt.typ b/spec/lt.typ index aecc93f41..cb4f9c141 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/lt.toml", config) -#show: book-page("lt.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/memory.typ b/spec/memory.typ index 6d1baae41..ec8735e49 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/page.toml", config) -#show: book-page("memory.typ") // TODO: can we get rid of this? +#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. diff --git a/spec/memw.typ b/spec/memw.typ index 29f183ced..77b786bf6 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -11,7 +11,7 @@ #let config = load_config() #let chip = load_chip("src/memw.toml", config) -#show: book-page("memw.typ") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/mul.typ b/spec/mul.typ index a2d231f6f..bc5898fa0 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -12,7 +12,7 @@ #let config = load_config() #let chip = load_chip("src/mul.toml", config) -#show: book-page("mul.typ") +#show: book-page(chip.name) #let mul = raw(chip.name) diff --git a/spec/shift.typ b/spec/shift.typ index 07def2327..177ce6104 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -14,7 +14,7 @@ #let shift = raw(chip.name) -#show: book-page("shift.typ") +#show: book-page(chip.name) == Interface The #shift chip has the following interface: