diff --git a/spec/add.typ b/spec/add.typ index 0dade7b01..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.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 diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 34ec6dd10..9b5b4a638 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(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/book.typ b/spec/book.typ index 29e61350c..b194b7f70 100644 --- a/spec/book.typ +++ b/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], ), + ("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, _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 + } +} diff --git a/spec/branch.typ b/spec/branch.typ index a18c252b7..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.with(title: "BRANCH chip") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/cpu.typ b/spec/cpu.typ index 784d750d2..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.with(title: "CPU chip") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/decode.typ b/spec/decode.typ index d8332e033..c68b1ae53 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, @@ -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. \ No newline at end of file +More details on this matter are provided in the `CPU` chip. 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..835751163 100644 --- a/spec/ebook.typ +++ b/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() 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..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.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. diff --git a/spec/load.typ b/spec/load.typ index 931611108..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.with(title: "LOAD chip") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/lt.typ b/spec/lt.typ index 3b57a62e3..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.with(title: "LT chip") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/memory.typ b/spec/memory.typ index 6687d733d..ec8735e49 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") 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][ diff --git a/spec/memw.typ b/spec/memw.typ index bcf6a64b0..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.with(title: "MEMW chip") +#show: book-page(chip.name) == Columns #let nr_variables = total_nr_variables(chip) diff --git a/spec/mul.typ b/spec/mul.typ index 1892994f0..bc5898fa0 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(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) diff --git a/spec/shift.typ b/spec/shift.typ index 70aebc97c..177ce6104 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(chip.name) == 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/templates/page.typ b/spec/templates/page.typ index 1f7f88ea0..4ec7b27ac 100644 --- a/spec/templates/page.typ +++ b/spec/templates/page.typ @@ -85,8 +85,11 @@ /// - 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", 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 +140,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 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.