diff --git a/spec/.gitignore b/spec/.gitignore index f425d1fde..d5cb26347 100644 --- a/spec/.gitignore +++ b/spec/.gitignore @@ -1,4 +1,3 @@ -dist/* -interaction_count.json -ebook.pdf +bundle/* +spec.pdf venv/* diff --git a/spec/README.md b/spec/README.md index da844e801..f28b671ad 100644 --- a/spec/README.md +++ b/spec/README.md @@ -2,18 +2,18 @@ Formal specification of the Lambda VM. Covers the per-chip AIR constraints (CPU, decode, bitwise, branch, LT, shift, MUL, DVRM, MEMW, LOAD, page, register, halt, commit, keccak), the memory argument, and the LogUp lookup framework that links the tables. -The specification is written in [Typst](https://typst.app/) and rendered as either a PDF or a browsable HTML wiki using [shiroa](https://myriad-dreamin.github.io/shiroa/). +The specification is written in [Typst](https://typst.app/) and rendered as either a PDF or a browsable bundle of web pages [Typst's HTML export](https://typst.app/docs/reference/bundle/). ## Rendering it locally 1. [Install Typst](https://github.com/typst/typst?tab=readme-ov-file#installation). -2. [Install shiroa](https://myriad-dreamin.github.io/shiroa/guide/installation.html). -3. From this directory, run: +2. From this directory, run: ```sh - shiroa serve + typst compile spec.typ ``` - - shiroa will host the HTML wiki locally and live-reload as you edit the `.typ` source files. - -To produce a PDF instead, see the shiroa documentation for the `build` command. + to compile the spec as a PDF (`spec.pdf`), or + ```sh + typst compile --features bundle,html --format bundle bundle.typ + ``` + to compile the web format to `bundle/`. diff --git a/spec/about_ecalls.typ b/spec/about_ecalls.typ index f4ae00a23..102d7a504 100644 --- a/spec/about_ecalls.typ +++ b/spec/about_ecalls.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -11,8 +11,6 @@ #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: diff --git a/spec/add.typ b/spec/add.typ index 1f597c083..a3e64f493 100644 --- a/spec/add.typ +++ b/spec/add.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, et +#import "/meta.typ": et #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions, @@ -6,8 +6,6 @@ #let chip = load_chip("src/add.toml", config) #let subchip = load_chip("src/sub.toml", config) -#show: book-page(chip.name) - #set_nr_interactions(chip, name: "SUB") #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 1babeefcc..e8507e44d 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let chip = load_chip("src/bitwise.toml", config) #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 diff --git a/spec/book.typ b/spec/book.typ deleted file mode 100644 index 052f134bd..000000000 --- a/spec/book.typ +++ /dev/null @@ -1,230 +0,0 @@ -#import "@preview/shiroa:0.3.1": * -#import "/templates/page.typ": project -#import "@preview/equate:0.3.2": equate - -#show: book - -#let meta = ( - title: "Lambda VM specification", - authors: ("3MI Labs", "Aligned"), - version: "0.2", - summary: ( - ("PROOF SYSTEM", ( - ("logup.typ", [`LogUp` argument], ), - ("memory.typ", [Memory argument], ), - ("streaming.typ", [Streaming prover], ), - )), - ("OVERVIEW", ( - ("variables.typ", [Variables], ), - ("signatures.typ", [Signatures], ), - )), - ("TEMPLATES", ( - ("is_bit.typ", [`IS_BIT` template], ), - ("is_byte.typ", [`IS_BYTE` template], ), - ("sign.typ", [`SIGN` template], ), - ("add.typ", [`ADD`/`SUB` template], ), - ("neg.typ", [`NEG` template], ), - ("reg.typ", [`REG`/`REGW` template], ), - )), - ("CPU", ( - ("decode.typ", [`DECODE` table], ), - ("cpu.typ", [`CPU` chip], ), - ("cpu32.typ", [`CPU32` chip], ), - )), - ("ALU", ( - ("shift.typ", [`SHIFT` chip], ), - ("branch.typ", [`BRANCH` chip], ), - ("lt.typ", [`LT` chip], ), - ("eq.typ", [`EQ` chip], ), - ("mul.typ", [`MUL` chip], ), - ("dvrm.typ", [`DVRM` chip], ), - ("bitwise.typ", [`BITWISE` chips], ), - ("bytewise.typ", [`BYTEWISE` chip], ) - )), - ("MEMORY", ( - ("memw.typ", [`MEMW` chip], ), - ("load.typ", [`LOAD` chip], ), - ("store.typ", [`STORE` chip], ), - )), - ("ECALLS", ( - ("about_ecalls.typ", [About `ECALL`], ), - ("halt.typ", [`HALT` chip], ), - ("commit.typ", [`COMMIT` chip], ), - ("sha256.typ", [`SHA256` accelerator], ), - ("keccak.typ", [`KECCAK` accelerator], ), - ("ecsm.typ", [`ECSM` accelerator], ), - ("fext.typ", [Extension field accelerator], ), - )), - ("MATHEMATICS", ( - ("limbs_and_carries.typ", [On limb decomposition and carries], ), - )) - ) -) -#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( - ((title, sections)) => { - heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join() - } - ).join() -) - -#let highlights = ( - "aside": ("Aside", rgb("55aaff")), - "attention": ("Attention", rgb("ff2600")), -) - -#let highlight(title, body, ref: none, kind: "aside") = [ - #figure( - caption: title, - supplement: highlights.at(kind).at(0), - kind: kind, - body - )#ref -] - -#let aside = highlight.with(kind: "aside") -#let attention = highlight.with(kind: "attention") - -#let common-formatting(body) = { - set footnote(numbering: "[1]") - show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) - show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") - show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { - set figure.caption(position: top) - show figure.caption: cap => block( - inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), - outset: (left: 1em), - width: 100% + 1em, - fill: highlights.at(it.kind).at(1), - stroke: luma(50%), - align(center, strong(text(fill: black, cap))) - ) - block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false, align(left, it)) - } - body -} - - -#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ - #set text(fill: foreground) - *TODO #if name != none { [(#name)] }*: #body -] -#let rj = todo.with(background: teal, name: "Robin") -#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") -#let cdsg = todo.with(background: olive, name: "Cyprien") - - -#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) = { - show ref: none - context { - place(hide(box(width: auto, height: 0%, strip-all(include "/" + f)))) - } -} - -// 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_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_sections.position(x => x == found) + 1)]) - } else { - // Because shiroa does weird url escaping - let shiroa-label = label(str(lbl).replace(":", "%3A")) - 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 - // 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) = { - if not file.ends-with(".typ") { - file = lower(file) + ".typ" - } - - 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 - context _toplevel.update(s => { - if s == none { - file - } else { - s - } - }) - let cond() = _toplevel.final() == file - show ref: it => context if cond() { xref(it) } - let title = context { - // Strip raw, because shiroa already makes the title raw - show raw: it => it.text - meta_sections.find(x => x.at(0) == _toplevel.final()).at(1) - } - project.with(..args, title: title, description: plain-text(meta_sections.find(x => x.at(0) == file).at(1)), cond: cond)([ - #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() { - xref-include(key) - }).join() - #metadata(json("interaction_count.json").sum(default: (:))) - - #let chapter-index = meta_sections.position(x => x.at(0) == file) + 1 - #set heading(numbering: (..args) => [#chapter-index.#numbering("1.1", ..args)]) - #counter(heading).update(0) - - #body - ]) - } - } else { - body => body - } -} diff --git a/spec/branch.typ b/spec/branch.typ index d6ab53a18..1909555e7 100644 --- a/spec/branch.typ +++ b/spec/branch.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #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. diff --git a/spec/build_shiroa.sh b/spec/build_shiroa.sh deleted file mode 100755 index 55a3c8d24..000000000 --- a/spec/build_shiroa.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/bin/env bash - -set -euo pipefail - -# cd into the script directory -cd "$(dirname "${BASH_SOURCE[0]}")" - -# Clean up potential old file -rm -f interaction_count.json - -# Always clean up after ourselves -trap 'rm -f interaction_count.json' EXIT - -# Query the ebook version for the proper counts -typst query ebook.typ '' --field value > interaction_count.json - -# Check if there's enough memory available for a parallel shiroa build -# 20GiB as comfortable baseline -available_kb=$(awk '/MemAvailable/ { print $2 }' /proc/meminfo) -required_kb=$((20 * 1024 * 1024)) -if [ "$available_kb" -lt "$required_kb" ]; then - echo "Falling back to single-thread" - export RAYON_NUM_THREADS=1 -fi - -# And build -shiroa build diff --git a/spec/bundle.typ b/spec/bundle.typ new file mode 100644 index 000000000..56772cebf --- /dev/null +++ b/spec/bundle.typ @@ -0,0 +1,143 @@ +#import "/meta.typ": meta, common-formatting, highlights + +#context assert(target() == "bundle", message: "Please compile this file only with `--format bundle`") + +#set document(author: meta.authors, title: meta.title) +#set heading(numbering: "1.1") +#show: common-formatting + +// Add an HTML attr to an element if not present. Helps guard against show rule recursion. +// `value` can also be a function depending on the element +#let add-attr(key, value) = it => { + if key in it.attrs { + it + } else { + let v = if type(value) == function { value(it) } else { value } + html.elem(it.tag, attrs: it.attrs + ((key):v), it.body) + } +} + +// HTML-specific stuff +// TODO: improve +#show pagebreak: none +#show align: it => it.body +#show grid: it => table(columns: it.columns, gutter: it.column-gutter, ..it.children.map(c => c.body)) +#show math.frac.where(style: "skewed"): it => math.frac(it.num, it.denom, style: "horizontal") +#show math.equation: it => { + show raw: r => r.text + it +} +#show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { + show html.elem.where(tag: "figure"): add-attr("data-kind", "highlight") + show html.elem.where(tag: "figcaption"): add-attr("style", "background-color:" + highlights.at(it.kind).at(1).to-hex() + ";color:" + highlights.at(it.kind).at(2).to-hex() + ";") + it +} +#show figure.where(kind: "thmenv"): fig => { + show html.elem.where(tag: "figure"): add-attr("data-kind", lower(repr(fig.supplement).slice(1, -1))) + show pad: it => it.body + show h: none + show figure.caption: none + show "∎": html.elem("mrow", attrs: ("class": "qed"), "") + fig +} +// TODO: todo callouts (rj/et/cdsg) +// TODO: table divider lines (vline/hline) +// TODO(a11y): replace table.header calls with custom functions to indicate "scope" (col/row/rowgroup) so that we can export that to the html th + +#let nav(chapter) = { + let content = meta.summary.map(((title, chapters)) => { + strong(title); + list(..chapters.map(((cname, ctitle, cref)) => { + if cname == chapter { + html.a(ctitle, href: "#", class: "current", aria-current: "page") + } else { + link(label("doc:" + str(cname)), ctitle) + } + })) + }).join() + + html.nav({ + html.div(class: "desktop-nav", content) + html.details(class: "mobile-nav", html.summary("Navigation") + content) + }) +} + +#let prev_next(chapter) = { + let rellink(label, title, rel) = { + show html.elem.where(tag: "a"): add-attr("rel", rel) + link(label, title) + } + + let flat = meta.summary.map(((_, chapters)) => chapters).sum(default: ()) + let index = flat.position(c => c.at(0) == chapter) + if index == none { + index = -1 + } + + html.nav(class: "prev-next", + html.div(class: "prev", + if index == 0 { + rellink(label("doc:index"), meta.title, "prev") + } else if index > 0 { + let (name, title, _) = flat.at(index - 1) + rellink(label("doc:" + name), title, "prev") + } + ) + + + html.div(class: "next", + if index < flat.len() - 1 { + let (name, title, _) = flat.at(index + 1) + rellink(label("doc:" + name), title, "next") + } + ) + ) +} + +#let chapter(filename, ctitle, mainbody) = [ + #let (doctitle, vistitle) = if ctitle == meta.title { + (ctitle, ctitle) + } else { + (ctitle + " | " + meta.title, meta.title + html.span(class: "subheader", ctitle)) + } + + #document("/" + filename + ".html", title: doctitle, { + html.link(href: "/style.css", rel: "stylesheet") + html.link(href: "/fonts.css", rel: "stylesheet") + html.link(href: "/sidenotes.css", rel: "stylesheet") + html.script(src: "/sidenotes.js", defer: true) + html.header(title(link(, vistitle))) + html.main(mainbody) + nav(filename) + prev_next(filename) + })#label("doc:"+filename) +] + +#asset("/style.css", read("style.css")) +#asset("/fonts.css", read("fonts.css")) +#asset("/sidenotes.css", read("sidenotes.css")) +#asset("/sidenotes.js", read("sidenotes.js")) + +// Bundled fonts +#for f in ( + read("fonts.css") + .matches(regex("url\\(\"([^\"]+)\"\\)")) + .map(m => m.captures.first()) +) { + asset("/" + f, read(f, encoding: none)) +} + +#chapter("index", meta.title, include "front.typ") +#for (partname, part) in meta.summary { + for (name, title, ref) in part { + chapter(name, title, [ + #heading(level: 1, title)#ref + #set heading(offset: 1) + #include name + ".typ" + ]) + } +} + + +// Waiting for something like https://github.com/typst/typst/issues/8309 +// #document("/spec.pdf", include "spec.typ") +// #document("/spec.html", include "spec.typ") diff --git a/spec/bytewise.typ b/spec/bytewise.typ index 452e4fdbc..d8bfb50a9 100644 --- a/spec/bytewise.typ +++ b/spec/bytewise.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #let chip = load_chip("src/bytewise.toml", config) - -#show: book-page(chip.name) #let bytewise = raw(chip.name) The #bytewise chip is an ALU chip that decomposes the input `DWordWL` values into bytes and diff --git a/spec/chip.typ b/spec/chip.typ index fc4fc279c..81785c39b 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -1,4 +1,4 @@ -#import "expr.typ": expr_to_code, expr_to_math, type_to_code +#import "expr.typ": expr_to_code, expr_to_math, type_to_code, flatten_code /// Computes the total number of variables in a `chip` #let total_nr_variables(chip) = { @@ -51,11 +51,6 @@ // store it as metadata under the `` label // with tag `chip.name`. This tag is overwritten by `name` when specified. #let set_nr_interactions(chip, name: none) = { - // Skip when building shiroa, since the web/chapter structure fails to converge properly - import "book.typ": is-shiroa - if is-shiroa { - return - } if name == none { name = chip.name } @@ -160,9 +155,9 @@ let render_def_iters(iters) = { (..for (name, ..args) in iters { if args.len() == 1 { - ([#raw(name) = #expr_to_code(args.at(0))],) + ([#flatten_code((raw(name), ` = `, expr_to_code(args.at(0))))],) } else if args.len() == 2 { - ([#raw(name) #sym.in `[`#expr_to_code(args.at(0)), #expr_to_code(args.at(1))`]`],) + ([#flatten_code((raw(name), ` `, raw(sym.in), ` [`, expr_to_code(args.at(0)), `, `, expr_to_code(args.at(1)), `]`))],) } else { assert(false, message: "Invalid def range: " + repr(name, ..args)) } @@ -256,7 +251,7 @@ // Render the iterators of `obj`. #let iters(obj) = { - iters_of(obj).map(iter => [#raw(iter.at(0))#sym.in`[`#expr_to_code(iter.at(1)),#expr_to_code(iter.at(2))`]`]).join("\n") + iters_of(obj).map(iter => flatten_code((raw(iter.at(0)), ` `, raw(sym.in), ` [`, expr_to_code(iter.at(1)), `, `, expr_to_code(iter.at(2)), `]`))).join("\n") } #let args_interaction_like(input, output) = { @@ -328,14 +323,14 @@ let kind = constraint.kind if kind == "interaction" { - raw(constraint.tag) + `[` + args_interaction_like(constraint.input, constraint.at("output", default: none)) + `]` + flatten_code(raw(constraint.tag) + `[` + args_interaction_like(constraint.input, constraint.at("output", default: none)) + `]`) } else if kind == "arith" { [#eval(constraint.constraint, mode: "markup")] } else if kind == "template" { let cond = if "cond" in constraint { $#expr_to_math(constraint.cond) arrow.r.double$ + " " } - cond + raw(constraint.tag) + `<` + args_interaction_like(constraint.input, constraint.at("output", default: none)) + `>` + cond + flatten_code(raw(constraint.tag) + `<` + args_interaction_like(constraint.input, constraint.at("output", default: none)) + `>`) } else { assert(false, message: "illegal constraint format: " + kind) } diff --git a/spec/commit.typ b/spec/commit.typ index f6fa166f4..14aa1dedc 100644 --- a/spec/commit.typ +++ b/spec/commit.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -10,8 +10,6 @@ render_chip_padding_table, ) -#show: book-page("commit.typ") - #let config = load_config() #let chip = load_chip("src/commit.toml", config) #let commit = raw(chip.name) diff --git a/spec/cpu.typ b/spec/cpu.typ index cb11661f3..be9c48472 100644 --- a/spec/cpu.typ +++ b/spec/cpu.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -13,7 +12,6 @@ #let config = load_config() #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. diff --git a/spec/cpu32.typ b/spec/cpu32.typ index a3c639cc7..56d0bccf9 100644 --- a/spec/cpu32.typ +++ b/spec/cpu32.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #let chip = load_chip("src/cpu32.toml", config) - -#show: book-page(chip.name) #let cpu32 = raw(chip.name) The #cpu32 chip is used to delegate the 32-bit instructions of the RV64I instruction set diff --git a/spec/decode.typ b/spec/decode.typ index 6defcdc84..8e923dbb3 100644 --- a/spec/decode.typ +++ b/spec/decode.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj, xref #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -9,10 +8,10 @@ render_chip_padding_table, ) #import "/expr.typ": expr_to_math +#import "/meta.typ": stripe_tables #let config = load_config() #let chip = load_chip("src/decode.toml", config) -#show: book-page(chip.name) #let decode = raw(chip.name) @@ -90,16 +89,13 @@ Further clarification is provided in the notes following the table. #let decoding_table(lines) = { show figure: set block(breakable: true) + show: stripe_tables figure(table( columns: (auto, auto, auto, auto, 1fr, auto), stroke: 0pt, inset: (right: .5em), align: (left, right, center, center, left, right), - fill: (_, y) => - // 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*], [*alu*], [*`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 af4a73cde..504952710 100644 --- a/spec/dvrm.typ +++ b/spec/dvrm.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -12,9 +11,6 @@ #let config = load_config() #let chip = load_chip("src/dvrm.toml", config) - -#show: book-page(chip.name) - #let dvrm = raw(chip.name) The #dvrm chip provides division and remainder functionality, both signed and unsigned. diff --git a/spec/ecsm.typ b/spec/ecsm.typ index 95e4ef67a..210c418ac 100644 --- a/spec/ecsm.typ +++ b/spec/ecsm.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside, attention +#import "/meta.typ": aside, attention #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -12,8 +12,6 @@ #let config = load_config() -#show: book-page("ecsm.typ") - #show math.equation.where(block: false): box #let ecsm_chip = load_chip("src/ecsm.toml", config) diff --git a/spec/eq.typ b/spec/eq.typ index 379df796d..ce24a7e2b 100644 --- a/spec/eq.typ +++ b/spec/eq.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #let chip = load_chip("src/eq.toml", config) - -#show: book-page(chip.name) #let eq = raw(chip.name) The #eq chip is an ALU chip that compares two values and outputs a bit indicating whether they are equal or not. diff --git a/spec/equate-lite.typ b/spec/equate-lite.typ new file mode 100644 index 000000000..1365bd23e --- /dev/null +++ b/spec/equate-lite.typ @@ -0,0 +1,194 @@ +// Hacks to make equate work (for our purposes) with HTML export +// Multiple parts copied and reworked from the equate source. +// For paged export, we just fall back to regular equate + +#import "@preview/equate:0.3.2": equate as equate-paged + +// Mostly copied +#let text-for(nums, numbering_, supplement) = { + let num = numbering( + if type(numbering) == str { + // Trim numbering pattern of prefix and suffix characters. + let counting-symbols = ("1", "a", "A", "i", "I", "一", "壹", "あ", "い", "ア", "イ", "א", "가", "ㄱ", "*", "①", "⓵") + let prefix-end = val.numbering.codepoints().position(c => c in counting-symbols) + let suffix-start = val.numbering.codepoints().rev().position(c => c in counting-symbols) + numbering_.slice(prefix-end, if suffix-start == 0 { none } else { -suffix-start }) + } else { + numbering_ + }, + ..nums + ) + + if supplement not in ([], none) [#supplement~#num] else [#num] +} + +#let equate-ref(it) = { + if it.element == none { return it } + if it.element.func() != metadata { return it } + + let val = it.element.value + + let supplement = if it.supplement == auto { + val.supplement + } else if type(it.supplement) == function { + assert(false, message: "Unsupported feature") + } else { + it.supplement + } + + html.a(href: "#" + str(it.target), text-for(val.nums, val.numbering, supplement)) +} + +#let show-rule() = it => context { + // Allow a way to make default equations. + if it.has("label") and it.label == { + return it + } + + // We assert that we're doing sub-numbering + state("equate/sub-numbering", false).update(_ => true) + + let body = it.body + let children = if repr(body.func()) == "sequence" { body.children } else { (body,) } + let lines = children.split(linebreak()).filter(line => line != ()) + + // Indices of lines that contain a label. + let labelled = lines + .enumerate() + .filter(((i, line)) => { + if line.len() == 0 { return false } + if line.last().func() != raw { return false } + if line.last().lang != "typc" { return false } + if line.last().text.match(regex("^<.+>$")) == none { return false } + return true + }) + .map(((i, _)) => i) + + // Indices of lines that are marked not to be numbered. + let revoked = lines + .enumerate() + .filter(((i, line)) => { + if i not in labelled { return false } + return line.last().text == "" + }) + .map(((i, _)) => i) + + // The "revoke" label shall not count as a labelled line. + labelled = labelled.filter(i => i not in revoked) + + // Indices of numbered lines in this equation. + let only-outer = labelled.len() == 0 and it.has("label") + if only-outer { + assert(revoked.len() == 0, message: "Don't revoke if the outer equation is labelled and no inner is") + } + let numbered = if only-outer { + // We place the outer label halfway + (lines.len() / 2,) + } else { + labelled + } + + // Main equation number. + let main-number = counter(math.equation).get() + + let new-lines = (lines + .enumerate() + .map(((i, line)) => { + if i in revoked { + // Remove "revoke" label and space and return line. + let _ = if line.at(-2, default: none) == [ ] { line.remove(-2) } + let _ = line.remove(-1) + return line + } + + let (lb, nums) = if i in labelled { + // Remove trailing spacing (before label). + let _ = if line.at(-2, default: none) == [ ] { line.remove(-2) } + // Remove the label + let lb = line.last().text.slice(1, -1) + let _ = line.remove(-1) + (lb, main-number + (numbered.position(n => n == i) + 1,)) + } else if only-outer { + (str(it.label), main-number) + } else { + return line + } + + let nm = numbering(it.numbering, ..nums) + line.push($ & $.body) + line.push(html.elem("mspace", attrs: ("width": "2em"))) + line.push(html.elem("mrow", attrs: ("id": lb, "aria-label": repr(it.supplement).slice(1, -1) + " " + numbering(it.numbering, ..nums)), nm)) + if not only-outer { + line.push([#metadata((nums: nums, numbering: it.numbering, supplement: it.supplement))#label(lb)]) + } + + line + })) + + // Whether the equation is numbered at all. + let has-numbering = it.numbering != none and type(it.numbering) in (str, function) + + // Whether this equation consumes an equation number. + let counted = has-numbering and numbered.len() > 0 + + // Step the counter only for equations that consume an equation number. + if not counted { + counter(math.equation).update(x => x - 1) + } + + [ + // The equation itself. It is emitted without numbering (the visible + // number is rendered as text), so that it does not step the counter. + #math.equation( + block: true, + numbering: it.numbering, + new-lines.join((linebreak(),)).join() + ) + + // The replaced equation steps the counter natively; revert that step. + #counter(math.equation).update(x => x - 1) + ] +} + +#let equate( + breakable: auto, + sub-numbering: false, + number-mode: "line", + debug: false, + body +) = { + assert( + sub-numbering == true + and breakable == true + and number-mode == "label", + message: "Unsupported equate-lite variant" + ) + + context { + if target() == "html" { + if type(body) == label { + { + show ref: equate-ref + ref(body) + } + } else if type(body) == content and body.func() == ref { + { + show ref: equate-ref + body + } + } else { + show math.equation.where(block: true): show-rule() + body + } + } else { + // Delegate to the original package for paged output. + show: equate-paged.with( + breakable: breakable, + sub-numbering: sub-numbering, + number-mode: number-mode, + debug: debug + ) + body + } + } +} diff --git a/spec/expr.typ b/spec/expr.typ index 11c20ef37..16ac94867 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -70,7 +70,7 @@ ) // Mutual recursion through a trick from https://github.com/typst/typst/issues/744 -#let make_expr_formatter(dict, empty: none, var: raw, num: str) = { +#let make_expr_formatter(dict, empty: none, var: raw, num: str, flatten: (x) => x) = { let res(pp, expr) = { if expr == none { empty @@ -79,9 +79,9 @@ } else if type(expr) == int { num(expr) } else if type(expr) == array { - (dict.at(expr.at(0), default: (pp, rec, e) => { + flatten((dict.at(expr.at(0), default: (pp, rec, e) => { assert(false, message: "Invalid expression: " + repr(e)) - }))(pp, res, expr) + }))(pp, res, expr)) } } res.with(PREC.MAX) @@ -96,6 +96,16 @@ } } +#let flatten_code(x) = { + if type(x) == array { + raw(x.map(c => flatten_code(c).text).join("")) + } else if x.has("children") { + flatten_code(x.children) + } else { + x + } +} + // Typeset an expression as code #let expr_to_code = make_expr_formatter( ( @@ -146,6 +156,8 @@ cwrap(rec(PREC.cast, e.at(1)) + ` as ` + type_to_code(e.at(2)), pp < PREC.cast) }, ), + num: (n) => raw(str(n)), + flatten: flatten_code ) // Wrap math `expr` if `apply = true` diff --git a/spec/fext.typ b/spec/fext.typ index 95f0ab4f5..7432f0f46 100644 --- a/spec/fext.typ +++ b/spec/fext.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -10,8 +10,6 @@ render_chip_padding_table, ) -#show: book-page("fext.typ") - #let config = load_config() #let loadchip = load_chip("src/fext_load.toml", config) #let load = raw(loadchip.name) diff --git a/spec/fonts.css b/spec/fonts.css new file mode 100644 index 000000000..665542b5c --- /dev/null +++ b/spec/fonts.css @@ -0,0 +1,78 @@ +/* + Bundled font faces, from the official releases (converted, where needed, to woff2). + License files are present in this directory: + + Presented in this format to ease regex extraction in bundle.typ :) + url("fonts/LICENSE-DejaVu.txt") + url("fonts/OFL-Libertinus.txt") + url("fonts/OFL-STIX.txt") + url("fonts/LICENSE-NewCMMath.txt") +*/ +@font-face { + font-family: 'Libertinus Serif'; + font-style: normal; + font-weight: 400; + src: local(Libertinus Serif), local(Libertinus Serif Regular), local(Libertinus), local(Linux Libertine), url("fonts/LibertinusSerif-Regular.woff2") format("woff2"); +} +@font-face { + font-family: 'Libertinus Serif'; + font-style: italic; + font-weight: 400; + src: local(Libertinus Serif Italic), url("fonts/LibertinusSerif-Italic.woff2") format("woff2"); +} +@font-face { + font-family: 'Libertinus Serif'; + font-style: normal; + font-weight: 600; + src: local(Libertinus Serif), local(Libertinus Serif Semibold), url("fonts/LibertinusSerif-Semibold.woff2") format("woff2"); +} +@font-face { + font-family: 'Libertinus Serif'; + font-style: normal; + font-weight: 700; + src: local(Libertinus Serif Bold), url("fonts/LibertinusSerif-Bold.woff2") format("woff2"); +} +@font-face { + font-family: 'Libertinus Serif'; + font-style: italic; + font-weight: 700; + src: local(Libertinus Serif Bold Italic), url("fonts/LibertinusSerif-BoldItalic.woff2") format("woff2"); +} + +@font-face { + font-family: 'New Computer Modern Math'; + font-style: normal; + font-weight: 400; + font-display: swap; + src: url("fonts/NewCMMath-Book.woff2") format("woff2"); +} +@font-face { + font-family: 'New Computer Modern Math'; + font-style: normal; + font-weight: 700; + font-display: swap; + src: url("fonts/NewCMMath-Bold.woff2") format("woff2"); +} + +@font-face { + font-family: 'STIX Two Text'; + font-style: normal; + font-weight: 400; + font-display: swap; + src: url("fonts/STIXTwoText-Regular.woff2") format("woff2"); +} + +@font-face { + font-family: 'DejaVu Sans Mono'; + font-style: normal; + font-weight: 400; + font-display: swap; + src: url("fonts/DejaVuSansMono.woff2") format("woff2"); +} +@font-face { + font-family: 'DejaVu Sans Mono'; + font-style: normal; + font-weight: 700; + font-display: swap; + src: url("fonts/DejaVuSansMono-Bold.woff2") format("woff2"); +} diff --git a/spec/fonts/DejaVuSansMono-Bold.woff2 b/spec/fonts/DejaVuSansMono-Bold.woff2 new file mode 100644 index 000000000..7248a750a Binary files /dev/null and b/spec/fonts/DejaVuSansMono-Bold.woff2 differ diff --git a/spec/fonts/DejaVuSansMono.woff2 b/spec/fonts/DejaVuSansMono.woff2 new file mode 100644 index 000000000..38dbb7ba8 Binary files /dev/null and b/spec/fonts/DejaVuSansMono.woff2 differ diff --git a/spec/fonts/LICENSE-DejaVu.txt b/spec/fonts/LICENSE-DejaVu.txt new file mode 100644 index 000000000..df52c1709 --- /dev/null +++ b/spec/fonts/LICENSE-DejaVu.txt @@ -0,0 +1,187 @@ +Fonts are (c) Bitstream (see below). DejaVu changes are in public domain. +Glyphs imported from Arev fonts are (c) Tavmjong Bah (see below) + + +Bitstream Vera Fonts Copyright +------------------------------ + +Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera is +a trademark of Bitstream, Inc. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of the fonts accompanying this license ("Fonts") and associated +documentation files (the "Font Software"), to reproduce and distribute the +Font Software, including without limitation the rights to use, copy, merge, +publish, distribute, and/or sell copies of the Font Software, and to permit +persons to whom the Font Software is furnished to do so, subject to the +following conditions: + +The above copyright and trademark notices and this permission notice shall +be included in all copies of one or more of the Font Software typefaces. + +The Font Software may be modified, altered, or added to, and in particular +the designs of glyphs or characters in the Fonts may be modified and +additional glyphs or characters may be added to the Fonts, only if the fonts +are renamed to names not containing either the words "Bitstream" or the word +"Vera". + +This License becomes null and void to the extent applicable to Fonts or Font +Software that has been modified and is distributed under the "Bitstream +Vera" names. + +The Font Software may be sold as part of a larger software package but no +copy of one or more of the Font Software typefaces may be sold by itself. + +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, +TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME +FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING +ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, +WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF +THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE +FONT SOFTWARE. + +Except as contained in this notice, the names of Gnome, the Gnome +Foundation, and Bitstream Inc., shall not be used in advertising or +otherwise to promote the sale, use or other dealings in this Font Software +without prior written authorization from the Gnome Foundation or Bitstream +Inc., respectively. For further information, contact: fonts at gnome dot +org. + +Arev Fonts Copyright +------------------------------ + +Copyright (c) 2006 by Tavmjong Bah. All Rights Reserved. + +Permission is hereby granted, free of charge, to any person obtaining +a copy of the fonts accompanying this license ("Fonts") and +associated documentation files (the "Font Software"), to reproduce +and distribute the modifications to the Bitstream Vera Font Software, +including without limitation the rights to use, copy, merge, publish, +distribute, and/or sell copies of the Font Software, and to permit +persons to whom the Font Software is furnished to do so, subject to +the following conditions: + +The above copyright and trademark notices and this permission notice +shall be included in all copies of one or more of the Font Software +typefaces. + +The Font Software may be modified, altered, or added to, and in +particular the designs of glyphs or characters in the Fonts may be +modified and additional glyphs or characters may be added to the +Fonts, only if the fonts are renamed to names not containing either +the words "Tavmjong Bah" or the word "Arev". + +This License becomes null and void to the extent applicable to Fonts +or Font Software that has been modified and is distributed under the +"Tavmjong Bah Arev" names. + +The Font Software may be sold as part of a larger software package but +no copy of one or more of the Font Software typefaces may be sold by +itself. + +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT +OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL +TAVMJONG BAH BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL +DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM +OTHER DEALINGS IN THE FONT SOFTWARE. + +Except as contained in this notice, the name of Tavmjong Bah shall not +be used in advertising or otherwise to promote the sale, use or other +dealings in this Font Software without prior written authorization +from Tavmjong Bah. For further information, contact: tavmjong @ free +. fr. + +TeX Gyre DJV Math +----------------- +Fonts are (c) Bitstream (see below). DejaVu changes are in public domain. + +Math extensions done by B. Jackowski, P. Strzelczyk and P. Pianowski +(on behalf of TeX users groups) are in public domain. + +Letters imported from Euler Fraktur from AMSfonts are (c) American +Mathematical Society (see below). +Bitstream Vera Fonts Copyright +Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream Vera +is a trademark of Bitstream, Inc. + +Permission is hereby granted, free of charge, to any person obtaining a copy +of the fonts accompanying this license (“Fonts”) and associated +documentation +files (the “Font Software”), to reproduce and distribute the Font Software, +including without limitation the rights to use, copy, merge, publish, +distribute, +and/or sell copies of the Font Software, and to permit persons to whom +the Font Software is furnished to do so, subject to the following +conditions: + +The above copyright and trademark notices and this permission notice +shall be +included in all copies of one or more of the Font Software typefaces. + +The Font Software may be modified, altered, or added to, and in particular +the designs of glyphs or characters in the Fonts may be modified and +additional +glyphs or characters may be added to the Fonts, only if the fonts are +renamed +to names not containing either the words “Bitstream” or the word “Vera”. + +This License becomes null and void to the extent applicable to Fonts or +Font Software +that has been modified and is distributed under the “Bitstream Vera” +names. + +The Font Software may be sold as part of a larger software package but +no copy +of one or more of the Font Software typefaces may be sold by itself. + +THE FONT SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, +TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME +FOUNDATION +BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL, +SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN +ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR +INABILITY TO USE +THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE. +Except as contained in this notice, the names of GNOME, the GNOME +Foundation, +and Bitstream Inc., shall not be used in advertising or otherwise to promote +the sale, use or other dealings in this Font Software without prior written +authorization from the GNOME Foundation or Bitstream Inc., respectively. +For further information, contact: fonts at gnome dot org. + +AMSFonts (v. 2.2) copyright + +The PostScript Type 1 implementation of the AMSFonts produced by and +previously distributed by Blue Sky Research and Y&Y, Inc. are now freely +available for general use. This has been accomplished through the +cooperation +of a consortium of scientific publishers with Blue Sky Research and Y&Y. +Members of this consortium include: + +Elsevier Science IBM Corporation Society for Industrial and Applied +Mathematics (SIAM) Springer-Verlag American Mathematical Society (AMS) + +In order to assure the authenticity of these fonts, copyright will be +held by +the American Mathematical Society. This is not meant to restrict in any way +the legitimate use of the fonts, such as (but not limited to) electronic +distribution of documents containing these fonts, inclusion of these fonts +into other public domain or commercial font collections or computer +applications, use of the outline data to create derivative fonts and/or +faces, etc. However, the AMS does require that the AMS copyright notice be +removed from any derivative versions of the fonts which have been altered in +any way. In addition, to ensure the fidelity of TeX documents using Computer +Modern fonts, Professor Donald Knuth, creator of the Computer Modern faces, +has requested that any alterations which yield different font metrics be +given a different name. + +$Id$ diff --git a/spec/fonts/LICENSE-NewCMMath.txt b/spec/fonts/LICENSE-NewCMMath.txt new file mode 100644 index 000000000..8ab0387f5 --- /dev/null +++ b/spec/fonts/LICENSE-NewCMMath.txt @@ -0,0 +1,650 @@ +NewComputerModern License + +All fonts are distributed under the GUST license except + +NewCM10-Regular, all NewCMUncial, and all NewCM*Devanagari which are + +distributed with GPL3 or later plus Font Exception (FE) plus +Distribution Exception (DE); see Section 7 of the GPL3 license below +and consult the documentation of NewCM for details. + +GNU GENERAL PUBLIC LICENSE +Version 3, 29 June 2007 + +Copyright © 2007 Free Software Foundation, Inc. + +Everyone is permitted to copy and distribute verbatim copies of this +license document, but changing it is not allowed. + +Preamble + +The GNU General Public License is a free, copyleft license for +software and other kinds of works. The licenses for most software and +other practical works are designed to take away your freedom to share +and change the works. By contrast, the GNU General Public License is +intended to guarantee your freedom to share and change all versions of +a program--to make sure it remains free software for all its +users. We, the Free Software Foundation, use the GNU General Public +License for most of our software; it applies also to any other work +released this way by its authors. You can apply it to your programs, +too. + +When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + +To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you +have certain responsibilities if you distribute copies of the +software, or if you modify it: responsibilities to respect the freedom +of others. + +For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + +Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + +For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + +Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the +manufacturer can do so. This is fundamentally incompatible with the +aim of protecting users' freedom to change the software. The +systematic pattern of such abuse occurs in the area of products for +individuals to use, which is precisely where it is most +unacceptable. Therefore, we have designed this version of the GPL to +prohibit the practice for those products. If such problems arise +substantially in other domains, we stand ready to extend this +provision to those domains in future versions of the GPL, as needed to +protect the freedom of users. + +Finally, every program is threatened constantly by software +patents. States should not allow patents to restrict development and +use of software on general-purpose computers, but in those that do, we +wish to avoid the special danger that patents applied to a free +program could make it effectively proprietary. To prevent this, the +GPL assures that patents cannot be used to render the program +non-free. + +The precise terms and conditions for copying, distribution and modification follow. + +TERMS AND CONDITIONS + +0. Definitions. + +“This License” refers to version 3 of the GNU General Public License. + +“Copyright” also means copyright-like laws that apply to other kinds +of works, such as semiconductor masks. + +“The Program” refers to any copyrightable work licensed under this +License. Each licensee is addressed as “you”. “Licensees” and +“recipients” may be individuals or organizations. + +To “modify” a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of +an exact copy. The resulting work is called a “modified version” of +the earlier work or a work “based on” the earlier work. + +A “covered work” means either the unmodified Program or a work based on the Program. + +To “propagate” a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + +To “convey” a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user +through a computer network, with no transfer of a copy, is not +conveying. + +An interactive user interface displays “Appropriate Legal Notices” to +the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + +1. Source Code. + +The “source code” for a work means the preferred form of the work for +making modifications to it. “Object code” means any non-source form of +a work. + +A “Standard Interface” means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + +The “System Libraries” of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +“Major Component”, in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + +The “Corresponding Source” for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. The Corresponding Source +need not include anything that users can regenerate automatically from +other parts of the Corresponding Source. + +The Corresponding Source for a work in source code form is that same work. + +2. Basic Permissions. + +All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + +You may make, run and propagate covered works that you do not convey, +without conditions so long as your license otherwise remains in +force. You may convey covered works to others for the sole purpose of +having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + +Conveying under any other circumstances is permitted solely under the +conditions stated below. Sublicensing is not allowed; section 10 makes +it unnecessary. + +3. Protecting Users' Legal Rights From Anti-Circumvention Law. + +No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + +When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such +circumvention is effected by exercising rights under this License with +respect to the covered work, and you disclaim any intention to limit +operation or modification of the work as a means of enforcing, against +the work's users, your or third parties' legal rights to forbid +circumvention of technological measures. + +4. Conveying Verbatim Copies. + +You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + +You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + +5. Conveying Modified Source Versions. + +You may convey a work based on the Program, or the modifications to produce it from the Program, in the form of source code under the terms of section 4, provided that you also meet all of these conditions: + +• a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + +• b) The work must carry prominent notices stating that it is released + under this License and any conditions added under section 7. This + requirement modifies the requirement in section 4 to “keep intact + all notices”. + +• c) You must license the entire work, as a whole, under this License + to anyone who comes into possession of a copy. This License will + therefore apply, along with any applicable section 7 additional + terms, to the whole of the work, and all its parts, regardless of + how they are packaged. This License gives no permission to license + the work in any other way, but it does not invalidate such + permission if you have separately received it. + +• d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your work + need not make them do so. + +A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +“aggregate” if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + +6. Conveying Non-Source Forms. + +You may convey a covered work in object code form under the terms of +sections 4 and 5, provided that you also convey the machine-readable +Corresponding Source under the terms of this License, in one of these +ways: + +• a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium customarily + used for software interchange. + +• b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a written + offer, valid for at least three years and valid for as long as you + offer spare parts or customer support for that product model, to + give anyone who possesses the object code either (1) a copy of the + Corresponding Source for all the software in the product that is + covered by this License, on a durable physical medium customarily + used for software interchange, for a price no more than your + reasonable cost of physically performing this conveying of source, + or (2) access to copy the Corresponding Source from a network server + at no charge. + +• c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This alternative + is allowed only occasionally and noncommercially, and only if you + received the object code with such an offer, in accord with + subsection 6b. + +• d) Convey the object code by offering access from a designated place + (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) that + supports equivalent copying facilities, provided you maintain clear + directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + +• e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + +A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + +A “User Product” is either (1) a “consumer product”, which means any +tangible personal property which is normally used for personal, +family, or household purposes, or (2) anything designed or sold for +incorporation into a dwelling. In determining whether a product is a +consumer product, doubtful cases shall be resolved in favor of +coverage. For a particular product received by a particular user, +“normally used” refers to a typical or common use of that class of +product, regardless of the status of the particular user or of the way +in which the particular user actually uses, or expects or is expected +to use, the product. A product is a consumer product regardless of +whether the product has substantial commercial, industrial or +non-consumer uses, unless such uses represent the only significant +mode of use of the product. + +“Installation Information” for a User Product means any methods, +procedures, authorization keys, or other information required to +install and execute modified versions of a covered work in that User +Product from a modified version of its Corresponding Source. The +information must suffice to ensure that the continued functioning of +the modified object code is in no case prevented or interfered with +solely because modification has been made. + +If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + +The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or +updates for a work that has been modified or installed by the +recipient, or for the User Product in which it has been modified or +installed. Access to a network may be denied when the modification +itself materially and adversely affects the operation of the network +or violates the rules and protocols for communication across the +network. + +Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + +7. Additional Terms. + +Font Exception (FE): + +As a special exception, if you create a document which uses this font, +and embed this font or unaltered portions of this font into the +document, this font does not by itself cause the resulting document to +be covered by the GNU General Public License. This exception does not +however invalidate any other reasons why the document might be covered +by the GNU General Public License. If you modify this font, you may +extend this exception to your version of the font, but you are not +obligated to do so. If you do not wish to do so, delete this exception +statement from your version. + +Distribution Exception (DE) + +If you distribute the fonts as they are in your program, and your +program follows a license compatible with GPL version 3 (or later) as +described in https://www.gnu.org/licenses/license-list.en.html these +fonts do not by themselves cause the resulting program to be covered +by the GNU General Public License. This exception does not however +invalidate any other reasons why the program might be covered by the +GNU General Public License. If however you distribute a copy of the +fonts that modifies either the glyphs (one or more) or the glyph-set +by adding or removing glyphs, this exception is invalidated and your +program has to follow GPL version 3 (or later). + +8. Termination. + +You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + +However, if you cease all violation of this License, then your license +from a particular copyright holder is reinstated (a) provisionally, +unless and until the copyright holder explicitly and finally +terminates your license, and (b) permanently, if the copyright holder +fails to notify you of the violation by some reasonable means prior to +60 days after the cessation. + +Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + +Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + +9. Acceptance Not Required for Having Copies. + +You are not required to accept this License in order to receive or run +a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + +10. Automatic Licensing of Downstream Recipients. + +Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + +An “entity transaction” is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + +You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + +11. Patents. + +A “contributor” is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's “contributor version”. + +A contributor's “essential patent claims” are all patent claims owned +or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, “control” includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + +Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + +In the following three paragraphs, a “patent license” is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To “grant” such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + +If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. “Knowingly relying” means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + +If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + +A patent license is “discriminatory” if it does not include within the +scope of its coverage, prohibits the exercise of, or is conditioned on +the non-exercise of one or more of the rights that are specifically +granted under this License. You may not convey a covered work if you +are a party to an arrangement with a third party that is in the +business of distributing software, under which you make payment to the +third party based on the extent of your activity of conveying the +work, and under which the third party grants, to any of the parties +who would receive the covered work from you, a discriminatory patent +license (a) in connection with copies of the covered work conveyed by +you (or copies made from those copies), or (b) primarily for and in +connection with specific products or compilations that contain the +covered work, unless you entered into that arrangement, or that patent +license was granted, prior to 28 March 2007. + +Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + +12. No Surrender of Others' Freedom. + +If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under +this License and any other pertinent obligations, then as a +consequence you may not convey it at all. For example, if you agree to +terms that obligate you to collect a royalty for further conveying +from those to whom you convey the Program, the only way you could +satisfy both those terms and this License would be to refrain entirely +from conveying the Program. + +13. Use with the GNU Affero General Public License. + +Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + +14. Revised Versions of this License. + +The Free Software Foundation may publish revised and/or new versions +of the GNU General Public License from time to time. Such new versions +will be similar in spirit to the present version, but may differ in +detail to address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies that a certain numbered version of the GNU General Public +License “or any later version” applies to it, you have the option of +following the terms and conditions either of that numbered version or +of any later version published by the Free Software Foundation. If the +Program does not specify a version number of the GNU General Public +License, you may choose any version ever published by the Free +Software Foundation. + +If the Program specifies that a proxy can decide which future versions +of the GNU General Public License can be used, that proxy's public +statement of acceptance of a version permanently authorizes you to +choose that version for the Program. + +Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + +15. Disclaimer of Warranty. + +THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM “AS IS” WITHOUT +WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND +PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE PROGRAM PROVE +DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR +CORRECTION. + +16. Limitation of Liability. + +IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR +CONVEYS THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES +ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT +NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR +LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM +TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER OR OTHER +PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. + +17. Interpretation of Sections 15 and 16. + +If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + +END OF TERMS AND CONDITIONS + +How to Apply These Terms to Your New Programs + +If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these +terms. + +To do so, attach the following notices to the program. It is safest to + attach them to the start of each source file to most effectively + state the exclusion of warranty; and each file should have at + least the “copyright” line and a pointer to where the full notice + is found. Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper +mail. If the program does terminal interaction, make it output a +short notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the +appropriate parts of the General Public License. Of course, your +program's commands might be different; for a GUI interface, you would +use an “about box”. + +You should also get your employer (if you work as a programmer) or +school, if any, to sign a “copyright disclaimer” for the program, if +necessary. For more information on this, and how to apply and follow +the GNU GPL, see . + +The GNU General Public License does not permit incorporating your +program into proprietary programs. If your program is a subroutine +library, you may consider it more useful to permit linking proprietary +applications with the library. If this is what you want to do, use the +GNU Lesser General Public License instead of this License. But first, +please read + diff --git a/spec/fonts/LibertinusSerif-Bold.woff2 b/spec/fonts/LibertinusSerif-Bold.woff2 new file mode 100644 index 000000000..2604c2070 Binary files /dev/null and b/spec/fonts/LibertinusSerif-Bold.woff2 differ diff --git a/spec/fonts/LibertinusSerif-BoldItalic.woff2 b/spec/fonts/LibertinusSerif-BoldItalic.woff2 new file mode 100644 index 000000000..c1d3632a9 Binary files /dev/null and b/spec/fonts/LibertinusSerif-BoldItalic.woff2 differ diff --git a/spec/fonts/LibertinusSerif-Italic.woff2 b/spec/fonts/LibertinusSerif-Italic.woff2 new file mode 100644 index 000000000..f9331a7d2 Binary files /dev/null and b/spec/fonts/LibertinusSerif-Italic.woff2 differ diff --git a/spec/fonts/LibertinusSerif-Regular.woff2 b/spec/fonts/LibertinusSerif-Regular.woff2 new file mode 100644 index 000000000..61938662c Binary files /dev/null and b/spec/fonts/LibertinusSerif-Regular.woff2 differ diff --git a/spec/fonts/LibertinusSerif-Semibold.woff2 b/spec/fonts/LibertinusSerif-Semibold.woff2 new file mode 100644 index 000000000..268c66e23 Binary files /dev/null and b/spec/fonts/LibertinusSerif-Semibold.woff2 differ diff --git a/spec/fonts/NewCMMath-Bold.woff2 b/spec/fonts/NewCMMath-Bold.woff2 new file mode 100644 index 000000000..015a9b91e Binary files /dev/null and b/spec/fonts/NewCMMath-Bold.woff2 differ diff --git a/spec/fonts/NewCMMath-Book.woff2 b/spec/fonts/NewCMMath-Book.woff2 new file mode 100644 index 000000000..57b452389 Binary files /dev/null and b/spec/fonts/NewCMMath-Book.woff2 differ diff --git a/spec/fonts/OFL-Libertinus.txt b/spec/fonts/OFL-Libertinus.txt new file mode 100644 index 000000000..e85f1f4c4 --- /dev/null +++ b/spec/fonts/OFL-Libertinus.txt @@ -0,0 +1,94 @@ +Copyright © 2012-2024 The Libertinus Project Authors, +with Reserved Font Name "Linux Libertine", "Biolinum", "STIX Fonts". + +This Font Software is licensed under the SIL Open Font License, Version 1.1. +This license is copied below, and is also available with a FAQ at: +http://scripts.sil.org/OFL + + +----------------------------------------------------------- +SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007 +----------------------------------------------------------- + +PREAMBLE +The goals of the Open Font License (OFL) are to stimulate worldwide +development of collaborative font projects, to support the font creation +efforts of academic and linguistic communities, and to provide a free and +open framework in which fonts may be shared and improved in partnership +with others. + +The OFL allows the licensed fonts to be used, studied, modified and +redistributed freely as long as they are not sold by themselves. The +fonts, including any derivative works, can be bundled, embedded, +redistributed and/or sold with any software provided that any reserved +names are not used by derivative works. The fonts and derivatives, +however, cannot be released under any other type of license. The +requirement for fonts to remain under this license does not apply +to any document created using the fonts or their derivatives. + +DEFINITIONS +"Font Software" refers to the set of files released by the Copyright +Holder(s) under this license and clearly marked as such. This may +include source files, build scripts and documentation. + +"Reserved Font Name" refers to any names specified as such after the +copyright statement(s). + +"Original Version" refers to the collection of Font Software components as +distributed by the Copyright Holder(s). + +"Modified Version" refers to any derivative made by adding to, deleting, +or substituting -- in part or in whole -- any of the components of the +Original Version, by changing formats or by porting the Font Software to a +new environment. + +"Author" refers to any designer, engineer, programmer, technical +writer or other person who contributed to the Font Software. + +PERMISSION & CONDITIONS +Permission is hereby granted, free of charge, to any person obtaining +a copy of the Font Software, to use, study, copy, merge, embed, modify, +redistribute, and sell modified and unmodified copies of the Font +Software, subject to the following conditions: + +1) Neither the Font Software nor any of its individual components, +in Original or Modified Versions, may be sold by itself. + +2) Original or Modified Versions of the Font Software may be bundled, +redistributed and/or sold with any software, provided that each copy +contains the above copyright notice and this license. These can be +included either as stand-alone text files, human-readable headers or +in the appropriate machine-readable metadata fields within text or +binary files as long as those fields can be easily viewed by the user. + +3) No Modified Version of the Font Software may use the Reserved Font +Name(s) unless explicit written permission is granted by the corresponding +Copyright Holder. This restriction only applies to the primary font name as +presented to the users. + +4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font +Software shall not be used to promote, endorse or advertise any +Modified Version, except to acknowledge the contribution(s) of the +Copyright Holder(s) and the Author(s) or with their explicit written +permission. + +5) The Font Software, modified or unmodified, in part or in whole, +must be distributed entirely under this license, and must not be +distributed under any other license. The requirement for fonts to +remain under this license does not apply to any document created +using the Font Software. + +TERMINATION +This license becomes null and void if any of the above conditions are +not met. + +DISCLAIMER +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT +OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE +COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL +DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM +OTHER DEALINGS IN THE FONT SOFTWARE. diff --git a/spec/fonts/OFL-STIX.txt b/spec/fonts/OFL-STIX.txt new file mode 100644 index 000000000..11b7b8e88 --- /dev/null +++ b/spec/fonts/OFL-STIX.txt @@ -0,0 +1,92 @@ +Copyright 2001-2021 The STIX Fonts Project Authors (https://github.com/stipub/stixfonts), with Reserved Font Name "TM Math". STIX Fonts™ is a trademark of The Institute of Electrical and Electronics Engineers, Inc. + +This Font Software is licensed under the SIL Open Font License, Version 1.1. +This license is copied below, and is also available with a FAQ at: +http://scripts.sil.org/OFL + +----------------------------------------------------------- +SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007 +----------------------------------------------------------- + +PREAMBLE +The goals of the Open Font License (OFL) are to stimulate worldwide +development of collaborative font projects, to support the font creation +efforts of academic and linguistic communities, and to provide a free and +open framework in which fonts may be shared and improved in partnership +with others. + +The OFL allows the licensed fonts to be used, studied, modified and +redistributed freely as long as they are not sold by themselves. The +fonts, including any derivative works, can be bundled, embedded, +redistributed and/or sold with any software provided that any reserved +names are not used by derivative works. The fonts and derivatives, +however, cannot be released under any other type of license. The +requirement for fonts to remain under this license does not apply +to any document created using the fonts or their derivatives. + +DEFINITIONS +"Font Software" refers to the set of files released by the Copyright +Holder(s) under this license and clearly marked as such. This may +include source files, build scripts and documentation. + +"Reserved Font Name" refers to any names specified as such after the +copyright statement(s). + +"Original Version" refers to the collection of Font Software components as +distributed by the Copyright Holder(s). + +"Modified Version" refers to any derivative made by adding to, deleting, +or substituting -- in part or in whole -- any of the components of the +Original Version, by changing formats or by porting the Font Software to a +new environment. + +"Author" refers to any designer, engineer, programmer, technical +writer or other person who contributed to the Font Software. + +PERMISSION & CONDITIONS +Permission is hereby granted, free of charge, to any person obtaining +a copy of the Font Software, to use, study, copy, merge, embed, modify, +redistribute, and sell modified and unmodified copies of the Font +Software, subject to the following conditions: + +1) Neither the Font Software nor any of its individual components, +in Original or Modified Versions, may be sold by itself. + +2) Original or Modified Versions of the Font Software may be bundled, +redistributed and/or sold with any software, provided that each copy +contains the above copyright notice and this license. These can be +included either as stand-alone text files, human-readable headers or +in the appropriate machine-readable metadata fields within text or +binary files as long as those fields can be easily viewed by the user. + +3) No Modified Version of the Font Software may use the Reserved Font +Name(s) unless explicit written permission is granted by the corresponding +Copyright Holder. This restriction only applies to the primary font name as +presented to the users. + +4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font +Software shall not be used to promote, endorse or advertise any +Modified Version, except to acknowledge the contribution(s) of the +Copyright Holder(s) and the Author(s) or with their explicit written +permission. + +5) The Font Software, modified or unmodified, in part or in whole, +must be distributed entirely under this license, and must not be +distributed under any other license. The requirement for fonts to +remain under this license does not apply to any document created +using the Font Software. + +TERMINATION +This license becomes null and void if any of the above conditions are +not met. + +DISCLAIMER +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT +OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE +COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL +DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM +OTHER DEALINGS IN THE FONT SOFTWARE. diff --git a/spec/fonts/STIXTwoText-Regular.woff2 b/spec/fonts/STIXTwoText-Regular.woff2 new file mode 100644 index 000000000..05a4e2527 Binary files /dev/null and b/spec/fonts/STIXTwoText-Regular.woff2 differ diff --git a/spec/front.typ b/spec/front.typ index d78b0a38e..ed2774aa0 100644 --- a/spec/front.typ +++ b/spec/front.typ @@ -1,11 +1,9 @@ -#import "/book.typ": project, meta +#import "/meta.typ": meta -#show: project.with(title: "", cond: () => true) - -#align(center, title(meta.title)) -#align(center)[_Version #meta.version _] -#align(center, meta.authors.join(", ")) +#title(meta.title) +_Version #meta.version _ +#meta.authors.join(", ") This is the specification for the #link("https://github.com/yetanotherco/lambda_vm/")[Lambda verifiable vm]. - +// You can additionally download #link()[a PDF version] or #link()[single-page HTML] of this specification]. diff --git a/spec/halt.typ b/spec/halt.typ index 930283a7b..a4bf8ab04 100644 --- a/spec/halt.typ +++ b/spec/halt.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -10,8 +10,6 @@ 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) diff --git a/spec/is_bit.typ b/spec/is_bit.typ index 5246a623a..94e9bd648 100644 --- a/spec/is_bit.typ +++ b/spec/is_bit.typ @@ -1,12 +1,9 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_constraint_table, set_nr_interactions, total_nr_variables #let config = load_config() #let chip = load_chip("src/is_bit.toml", config) -#show: book-page(chip.name) - #set_nr_interactions(chip) #let nr_variables = total_nr_variables(chip) diff --git a/spec/is_byte.typ b/spec/is_byte.typ index 09bf78e98..c674c6959 100644 --- a/spec/is_byte.typ +++ b/spec/is_byte.typ @@ -1,11 +1,8 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_constraint_table, compute_nr_interactions, total_nr_variables, total_nr_instantiated_columns #let config = load_config() #let chip = load_chip("src/is_byte.toml", config) - -#show: book-page(chip.name) #let is_byte = raw(chip.name) #is_byte is a constraint template that is used to assert that a variable lies in the range $[0, 255]$ under the condition that `cond` is non-zero. Note: when `cond` is omitted, it defaults to $1$. @@ -19,4 +16,4 @@ The #is_byte template leverages #nr_interactions interaction(s): #render_chip_variable_table(chip, config) = Constraints -#render_constraint_table(chip, config) \ No newline at end of file +#render_constraint_table(chip, config) diff --git a/spec/keccak.typ b/spec/keccak.typ index 2f1e28499..8b918fd7e 100644 --- a/spec/keccak.typ +++ b/spec/keccak.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( compute_nr_interactions, @@ -12,8 +11,6 @@ #let config = load_config() #let chip = load_chip("src/keccak.toml", config) - -#show: book-page(chip.name) #let keccak = raw(chip.name) The #keccak chip applies the keccak permutation $kappa$ to a given memory range; diff --git a/spec/limbs_and_carries.typ b/spec/limbs_and_carries.typ index fb7404493..759159585 100644 --- a/spec/limbs_and_carries.typ +++ b/spec/limbs_and_carries.typ @@ -1,21 +1,11 @@ -#import "/book.typ": book-page -#import "@preview/ctheorems:1.1.3": * -#import "@preview/equate:0.3.2": equate - - -// Theorem/lemma formatting -#show: thmrules.with(qed-symbol: $square$) -#let lemma = thmbox("lemma", "Lemma", fill: rgb("#eee"),base_level: 0) -#let corollary = thmbox("lemma", "Corollary", fill: rgb("#eee"), base_level: 0) -#let proof = thmproof("proof", "Proof") +#import "meta.typ": lemma, corollary, proof +#import "equate-lite.typ": equate // Equation formatting #show: equate.with(breakable: true, sub-numbering: true, number-mode: "label") #set math.equation(numbering: "(1.1)") #show math.equation.where(block: false): box -#show: book-page("limbs_and_carries.typ") - In this section, we discuss, in order, + the multiplication and addition of limb-decomposed integers (involving carries), + prove an upper bound on the size of the carries in terms of the number of @@ -53,19 +43,19 @@ $ &= sum_(i=0)^(n-1) (sum_(j=0)^(n-1) (sum_(m in [mu]) vec(x)^((m))_i dot vec(y)^((m))_j dot L^(i+j)) + sum_(a in [alpha]) vec(z)^((a))_i dot L^i )\ &= sum_(r=0)^(2(n-1)) (sum_(j=0)^(r) (sum_(m in [mu]) vec(x)^((m))_(r-j) dot vec(y)^((m))_j dot L^r) + sum_(a in [alpha]) vec(z)^((a))_r dot L^r )\ &= sum_(r=0)^(2(n-1)) (sum_(j=0)^(r) (sum_(m in [mu]) vec(x)^((m))_(r-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_r) dot L^r\ - &= sum_(r=0)^(2(n-1)) overline(w)_r dot L^r, # + &= sum_(r=0)^(2(n-1)) dash(w)_r dot L^r, # $ where $ - overline(w)_i := sum_(m in [mu]) (sum_(j=0)^(i) vec(x)^((m))_(i-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_i. + dash(w)_i := sum_(m in [mu]) (sum_(j=0)^(i) vec(x)^((m))_(i-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_i. $ While @limbs:eq:f-semi-decomposition closely resembles that of a limb-decomposition (@limbs:eq:decomposition), -there is the problem that $overline(w)_i$ will generally not be bounded by $L$. -We therefore introduce a helper sequence, $c_i$, to transform $overline(w)_i$ into a proper decomposition $w_i$ as: +there is the problem that $dash(w)_i$ will generally not be bounded by $L$. +We therefore introduce a helper sequence, $c_i$, to transform $dash(w)_i$ into a proper decomposition $w_i$ as: $ - w_i &:= overline(w)_i + c_(i-1) mod L &text("for") i >= 0,\ - c_i &:= (overline(w)_i + c_(i-1) - w_i )/L &text("for") i >= 0,\ + w_i &:= dash(w)_i + c_(i-1) mod L &text("for") i >= 0,\ + c_i &:= (dash(w)_i + c_(i-1) - w_i )/L &text("for") i >= 0,\ $ with $c_i in NN$ and $c_(-1) := 0$. Note that these $c_i$ effectively move the "overflow" from one limb to the next limb up; @@ -78,19 +68,19 @@ they're commonly referred to as the _carry_ values. if and only if $c_(g-1) = 0$. ] #proof[ - Reordering the definition of $c_i$, we find the equality $w_i = overline(w)_i + c_(i-1) - c_i dot L$. + Reordering the definition of $c_i$, we find the equality $w_i = dash(w)_i + c_(i-1) - c_i dot L$. Leveraging this, we see that $ sum_(r=0)^(g-1) w_r dot L^r - &= sum_(r=0)^(g-1) (overline(w)_r + c_(r-1) - c_r dot L) dot L^r\ - &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + (sum_(s=0)^(g-1) c_(s-1) dot L^s) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ - &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + (sum_(s=-1)^(g-2) c_(s) dot L^(s+1)) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ - &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) + c_(-1) - c_(g-1) dot L^(g-1+1)\ - &= (sum_(r=0)^(g-1) overline(w)_r dot L^r) - c_(g-1) dot L^(g),\ - &= (sum_(r=0)^(2(n-1)) overline(w)_r dot L^r) - c_(g-1) dot L^(g),\ + &= sum_(r=0)^(g-1) (dash(w)_r + c_(r-1) - c_r dot L) dot L^r\ + &= (sum_(r=0)^(g-1) dash(w)_r dot L^r) + (sum_(s=0)^(g-1) c_(s-1) dot L^s) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ + &= (sum_(r=0)^(g-1) dash(w)_r dot L^r) + (sum_(s=-1)^(g-2) c_(s) dot L^(s+1)) - (sum_(t=0)^(g-1) c_t dot L^(t+1))\ + &= (sum_(r=0)^(g-1) dash(w)_r dot L^r) + c_(-1) - c_(g-1) dot L^(g-1+1)\ + &= (sum_(r=0)^(g-1) dash(w)_r dot L^r) - c_(g-1) dot L^(g),\ + &= (sum_(r=0)^(2(n-1)) dash(w)_r dot L^r) - c_(g-1) dot L^(g),\ &= f_(mu, alpha)(vec(x), vec(y), vec(z)) - c_(g-1) dot L^(g),\ $ - where the second-to-last step follows from the observation that $overline(w)_j = 0$ for $j > 2(n-1)$. + where the second-to-last step follows from the observation that $dash(w)_j = 0$ for $j > 2(n-1)$. We conclude that $w_i$ is a proper $g$-limb decomposition of $w$ if and only if $c_(g-1) = 0$. ] @@ -108,14 +98,14 @@ To bound for which $g$ we can guarantee that $c_(g-1) = 0$, we prove two upper b #proof[ Since $w_i in [L]$, $c_i - := frac((overline(w)_i + c_(i-1) - w_i ), L, style: "horizontal") - = floor.l frac((overline(w)_i + c_(i-1)), L, style: "horizontal") floor.r.$ - Hence, $c_i$ is maximized when both $overline(w)_i$ and $c_(i-1)$ are, and thus, - by induction, when $overline(w)_j$ is maximized for all $j <= i$. + := frac((dash(w)_i + c_(i-1) - w_i ), L, style: "horizontal") + = floor.l frac((dash(w)_i + c_(i-1)), L, style: "horizontal") floor.r.$ + Hence, $c_i$ is maximized when both $dash(w)_i$ and $c_(i-1)$ are, and thus, + by induction, when $dash(w)_j$ is maximized for all $j <= i$. Given that for all $m in [mu], a in [alpha], i in [n]: vec(x)^((m))_i, vec(y)^((m))_i, vec(z)^((a))_i <= L-1$, it follows that $ - &overline(w)_0 + &dash(w)_0 &=& sum_(m in [mu]) (vec(x)^((m))_0 dot vec(y)^((m))_0) + sum_(a in [alpha]) vec(z)^((a))_0\ &&<=& mu (L - 1)^2 + alpha (L-1)\ &&=& mu (L - 2)L + mu + (alpha - delta) L + delta L - alpha\ @@ -128,7 +118,7 @@ To bound for which $g$ we can guarantee that $c_(g-1) = 0$, we prove two upper b where $delta := delta_(mu < alpha)$. Assuming the statement holds for up to some $i >= 0$, we find that $ - overline(w)_(i+1) + dash(w)_(i+1) &= sum_(m in [mu]) (sum_(j=0)^(i+1) vec(x)^((m))_(i+1-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_(i+1) \ &<= mu (i+2)(L-1)^2 + alpha (L-1),\ c_(i+1) @@ -153,7 +143,7 @@ To achieve a tight upper bound for $i >= n$, we introduce a second lemma: #proof[ Starting with $k=0$, we find $ - overline(w)_n + dash(w)_n &= sum_(m in [mu]) (sum_(j=0)^(n) vec(x)^((m))_(n-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_n\ &<= mu (n-1) (L-1)^2 $ @@ -161,7 +151,7 @@ To achieve a tight upper bound for $i >= n$, we introduce a second lemma: Applying this upper bound to $c_n$, we obtain $ c_(n) - &= lr(floor.l (overline(w)_n + c_(n-1))/ L floor.r)\ + &= lr(floor.l (dash(w)_n + c_(n-1))/ L floor.r)\ &<= lr(floor.l (mu (n-1) (L-1)^2 + mu n (L-1) + alpha - mu - delta)/ L floor.r)\ &= lr(floor.l (mu (n-1) (L-2)L + mu (n-1) + mu n (L-1) + alpha - mu - delta) / L floor.r)\ &= lr(floor.l (mu (n-1) (L-2)L + (mu n - delta') L + delta'L + alpha - 2mu - delta) / L floor.r)\ @@ -171,7 +161,7 @@ To achieve a tight upper bound for $i >= n$, we introduce a second lemma: where $delta' := delta_(alpha < 2mu + delta)$. When the bound holds for some $i=n+k-1$ with $k in [1, n)$, it follows that $ - overline(w)_(n+k) + dash(w)_(n+k) &= sum_(m in [mu]) (sum_(j=0)^(n+k) vec(x)^((m))_(n+k-j) dot vec(y)^((m))_j) + sum_(a in [alpha]) vec(z)^((a))_(n+k)\ &<= mu (n-k-1) (L-1)^2\ c_(n+k) @@ -195,50 +185,50 @@ Combining both upper bounds, we now find that Given $alpha in [L]$ and $mu in [L/2]$ where at least one of the two is non-zero, then for all $i <= 2n$: $ -c_i <= &max(&max_(i in [n]) #h(1em) mu (i+1) (L-1) + alpha - mu - delta,\ +c_i &<= max(&max_(i in [n]) #h(1em) mu (i+1) (L-1) + alpha - mu - delta,\ &max_(k in [n]) #h(1em) mu (n-k-1)(L-2) + mu (n-k) - delta')\ -&= max(& mu n (L-1) + alpha - mu - delta, mu (n-1)(L-2) + mu n - delta')\ -&= mu n (L-1) + max(& alpha - mu - delta, - mu (L-2) - delta'). +&= max(mu n (L-1) + alpha - mu - delta, mu (n-1)(L-2) + mu n - delta')\ +&= mu n (L-1) + max(alpha - mu - delta, - mu (L-2) - delta'). $ Note that this simplifies to $mu n (L-1) + alpha - mu - delta$ for $L >= 4$. ] = Proof of Correctness -Lastly, we prove that there exists a correct method of constraining the relation between $overline(w)_i$, $w_i$ and $c_i$ inside this VM: +Lastly, we prove that there exists a correct method of constraining the relation between $dash(w)_i$, $w_i$ and $c_i$ inside this VM: #lemma("Constraint correctness")[ Let $L >= 4$, and $c_i, w_i in FF_p$ with $p$ prime. The constraints $ - c_i &= (overline(w)_i + c_(i-1) - w_i) dot L^(-1), #\ + c_i &= (dash(w)_i + c_(i-1) - w_i) dot L^(-1), #\ c_i &in [C], #\ c_(-1) &= 0, #\ w_i &in [L] # $ - together enforce $w_i = overline(w)_i + c_(i-1) mod L$ as long as $C in [mu n L + alpha, frac(p,L, style:"horizontal"))$. + together enforce $w_i = dash(w)_i + c_(i-1) mod L$ as long as $C in [mu n L + alpha, frac(p,L, style:"horizontal"))$. ] #proof[ Combining @limbs:eq:def_ci and @limbs:eq:range_ci, we find that $ &&c_i &in [C]\ - &<=>& overline(w)_i + c_(i-1) - w_i &in {0, L, ..., (C-1)L},\ - &<=>& w_i &in {overline(w)_i + c_(i-1), overline(w)_i + c_(i-1) - L, ..., overline(w)_i + c_(i-1) - (C-1)L}. + &<=>& dash(w)_i + c_(i-1) - w_i &in {0, L, ..., (C-1)L},\ + &<=>& w_i &in {dash(w)_i + c_(i-1), dash(w)_i + c_(i-1) - L, ..., dash(w)_i + c_(i-1) - (C-1)L}. $ Let us use $X_(i)$ to refer to this last set. Now --- under the assumption that $c_(i-1)$ is correct --- - observe that $w_i := overline(w)_i + c_(i-1) mod L in X_i$, since + observe that $w_i := dash(w)_i + c_(i-1) mod L in X_i$, since $ - overline(w)_i + c_(i-1) + dash(w)_i + c_(i-1) &<= (mu n (L-1)^2 + alpha (L-1)) + (mu (n-1) (L-1) + alpha - mu - delta)\ &<= mu n L^2 + alpha L\ &<= C L,\ $ where the utilized upper bound - $overline(w)_i <= mu n(L-1)^2 + alpha (L-1)$ + $dash(w)_i <= mu n(L-1)^2 + alpha (L-1)$ can be extracted from the proofs of @limbs:lm:carry-upperbound-pt1 and @limbs:lm:carry-upperbound-pt2, while the upper bound for $c_(i-1)$ follows from @limbs:cor:carry-upper-bound. Moreover, observe that $|X_i inter [L]| <= 1$ since $0 <= C L < p$. - Constraint @limbs:eq:range_wi therefore enforces that $w_i = overline(w)_i + c_(i-1) mod L$ if $c_(i-1)$ (and therefore $w_(i-1)$) is correct, - and as a result, $c_i = floor.l frac((overline(w)_i + c_(i-1)), L, style: "horizontal") floor.r$ is correct. + Constraint @limbs:eq:range_wi therefore enforces that $w_i = dash(w)_i + c_(i-1) mod L$ if $c_(i-1)$ (and therefore $w_(i-1)$) is correct, + and as a result, $c_i = floor.l frac((dash(w)_i + c_(i-1)), L, style: "horizontal") floor.r$ is correct. The proof now follows by induction, with @limbs:eq:c_-1_is_zero enforcing the base case. ] diff --git a/spec/load.typ b/spec/load.typ index ac469ec79..e9baf6540 100644 --- a/spec/load.typ +++ b/spec/load.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #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. diff --git a/spec/logup.typ b/spec/logup.typ index 038d67a8c..51cf51e19 100644 --- a/spec/logup.typ +++ b/spec/logup.typ @@ -1,6 +1,5 @@ -#import "/book.typ": book-page, aside, cdsg +#import "/meta.typ": aside, cdsg -#show: book-page("logup") #show link: underline #show "constraint choice": link()[constraint choice] diff --git a/spec/lt.typ b/spec/lt.typ index 6dd60b236..626077a6f 100644 --- a/spec/lt.typ +++ b/spec/lt.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #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. diff --git a/spec/memory.typ b/spec/memory.typ index b3bc8c092..2e6df7267 100644 --- a/spec/memory.typ +++ b/spec/memory.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, rj, aside, xref +#import "/meta.typ": rj, aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +12,6 @@ #let config = load_config() #let chip = load_chip("src/page.toml", config) -#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. That is, every byte read from some address corresponds to the byte that was last written to that address diff --git a/spec/memw.typ b/spec/memw.typ index 5d64e0f9d..b6a140c96 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,9 +11,6 @@ #let config = load_config() #let chip = load_chip("src/memw.toml", config) - -#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) diff --git a/spec/meta.typ b/spec/meta.typ new file mode 100644 index 000000000..fc6bc783b --- /dev/null +++ b/spec/meta.typ @@ -0,0 +1,127 @@ +#import "@preview/ctheorems:1.1.3": thmrules, thmbox, thmproof +#import "equate-lite.typ": equate + +#let meta = ( + title: "Lambda VM specification", + authors: ("3MI Labs", "Aligned"), + version: "0.2", + summary: ( + ("PROOF SYSTEM", ( + ("logup", [`LogUp` argument], ), + ("memory", [Memory argument], ), + ("streaming", [Streaming prover], ), + )), + ("OVERVIEW", ( + ("variables", [Variables], ), + ("signatures", [Signatures], ), + )), + ("TEMPLATES", ( + ("is_bit", [`IS_BIT` template], ), + ("is_byte", [`IS_BYTE` template], ), + ("sign", [`SIGN` template], ), + ("add", [`ADD`/`SUB` template], ), + ("neg", [`NEG` template], ), + ("reg", [`REG`/`REGW` template], ), + )), + ("CPU", ( + ("decode", [`DECODE` table], ), + ("cpu", [`CPU` chip], ), + ("cpu32", [`CPU32` chip], ), + )), + ("ALU", ( + ("shift", [`SHIFT` chip], ), + ("branch", [`BRANCH` chip], ), + ("lt", [`LT` chip], ), + ("eq", [`EQ` chip], ), + ("mul", [`MUL` chip], ), + ("dvrm", [`DVRM` chip], ), + ("bitwise", [`BITWISE` chips], ), + ("bytewise", [`BYTEWISE` chip], ) + )), + ("MEMORY", ( + ("memw", [`MEMW` chip], ), + ("load", [`LOAD` chip], ), + ("store", [`STORE` chip], ), + )), + ("ECALLS", ( + ("about_ecalls", [About `ECALL`], ), + ("halt", [`HALT` chip], ), + ("commit", [`COMMIT` chip], ), + ("sha256", [`SHA256` accelerator], ), + ("keccak", [`KECCAK` accelerator], ), + ("ecsm", [`ECSM` accelerator], ), + ("fext", [Extension field accelerator], ), + )), + ("MATHEMATICS", ( + ("limbs_and_carries", [On limb decomposition and carries], ), + )) + ) +) + +#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[ + #set text(fill: foreground) + *TODO #if name != none { [(#name)] }*: #body +] + +#let rj = todo.with(background: teal, name: "Robin") +#let et = todo.with(background: rgb("d4aa3a"), name: "Erik") +#let cdsg = todo.with(background: olive, name: "Cyprien") + + +/* Colors from the 3MI brand guidelines */ +#let highlights = ( + "aside": ("Aside", rgb("ffd700"), rgb("#1a1a1a")), + "attention": ("Attention", rgb("b3261e"), white), +) + +#let highlight(title, body, ref: none, kind: "aside") = [ + #figure( + caption: title, + supplement: highlights.at(kind).at(0), + kind: kind, + body + )#ref +] + +#let aside = highlight.with(kind: "aside") +#let attention = highlight.with(kind: "attention") + +#let stripe_tables(body) = context if target() == "html" { + show table: it => html.div(class: "striped", it) + body +} else if target() == "paged" { + set table(fill: (_, y) => if calc.odd(y) { color.rgb(255, 215, 0, 10%) } else { color.rgb(255, 255, 255, 20) }) + body +} else { + assert(false, message: "Unsupported target: " + target()) +} + +#let common-formatting(body) = { + set footnote(numbering: "[1]") + show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt) + show ref: equate.with(sub-numbering: true, breakable: true, number-mode: "label") + show selector.or(..highlights.keys().map(k => figure.where(kind: k))): it => { + set figure.caption(position: top) + show figure.caption: cap => block( + inset: (left: 1em, right: 1em, top: .75em, bottom: .75em), + outset: (left: 1em), + width: 100% + 1em, + fill: highlights.at(it.kind).at(1), + stroke: rgb("#d7d5cd"), + align(center, strong(text(fill: highlights.at(it.kind).at(2), cap))) + ) + block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: rgb("#d7d5cd"), breakable: false, align(left, it)) + } + show: it => context if target() == "paged" { + thmrules.with(qed-symbol: $square$)(it) + } else { + // Don't apply full thmrules, so we can do the html styling ourselves in bundle.typ + it + } + body +} + +// Theorem/lemma formatting +#let lemma = thmbox("lemma", "Lemma", fill: rgb("#f2f1ed"), base_level: 0) +#let corollary = thmbox("lemma", "Corollary", fill: rgb("#f2f1ed"), base_level: 0) +#let proof = thmproof("proof", "Proof") diff --git a/spec/mul.typ b/spec/mul.typ index e5dc0de7c..ab1d9ba41 100644 --- a/spec/mul.typ +++ b/spec/mul.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -12,9 +11,6 @@ #let config = load_config() #let chip = load_chip("src/mul.toml", config) - -#show: book-page(chip.name) - #let mul = raw(chip.name) The #mul chip constrains multiplication, both signed and unsigned, diff --git a/spec/neg.typ b/spec/neg.typ index 336152892..23926290b 100644 --- a/spec/neg.typ +++ b/spec/neg.typ @@ -1,10 +1,9 @@ -#import "/book.typ": book-page, aside, et +#import "/meta.typ": aside, et #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, compute_nr_interactions, #let config = load_config() #let chip = load_chip("src/neg.toml", config) -#show: book-page(chip.name) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/reg.typ b/spec/reg.typ index 6b294dc49..519535057 100644 --- a/spec/reg.typ +++ b/spec/reg.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, render_constraint_table, set_nr_interactions, @@ -8,8 +7,6 @@ #let read = raw(reg_read.name) #let write = raw(reg_write.name) -#show: book-page("REG") - We provide the #read and #write templates. These templates act as short hand notation for `MEMW` interactions pertaining to operations in the `register` domain ($= 1$, see @memory). diff --git a/spec/sha256.typ b/spec/sha256.typ index d72d5fc7a..f9520ddb4 100644 --- a/spec/sha256.typ +++ b/spec/sha256.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page, aside, rj +#import "/meta.typ": aside #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -11,8 +11,6 @@ #let config = load_config() -#show: book-page("sha256.typ") - #let sha256chip = load_chip("src/sha256.toml", config) #let sha256msgschedchip = load_chip("src/sha256msgsched.toml", config) #let sha256roundchip = load_chip("src/sha256round.toml", config) diff --git a/spec/shift.typ b/spec/shift.typ index a1583e3e7..2c5840fc5 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, et #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_variable_table, @@ -12,17 +11,14 @@ #let config = load_config() #let chip = load_chip("src/shift.toml", config) - #let shift = raw(chip.name) -#show: book-page(chip.name) - The #shift chip is designed to constrain that $ #`shifted` := cases( - #`in` #`<<` #`s` " if" #`direction` = 0, - #`in` #`>>` #`s` " if" #`direction` = 1 and #`signed` = 0, - #`in` #`>>>` #`s` "if" #`direction` = 1 and #`signed` = 1, + #`in` << #`s` " if" #`direction` = 0, + #`in` >> #`s` " if" #`direction` = 1 and #`signed` = 0, + #`in` >>> #`s` "if" #`direction` = 1 and #`signed` = 1, ) $ where @@ -32,7 +28,7 @@ $ #`shift` mod 64 "if" #`word_instr` = 0, ) $ -Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. +Here, $<<$ and $>>$ denote the _logical_ left and right shift operations, while $>>>$ denotes the _arithmetic_ right shift operation. = Variables #let nr_variables = total_nr_variables(chip) diff --git a/spec/sidenotes.css b/spec/sidenotes.css new file mode 100644 index 000000000..2f1c72d42 --- /dev/null +++ b/spec/sidenotes.css @@ -0,0 +1,49 @@ +.sidenote { + /* See also `style.css` */ + --gap-size-h: 24px; + --main-margin-width: calc((100vw - var(--content-max-width)) / 2); + /* max width of 280 px, otherwise fill the space except for gap-size-h */ + --note-width: min(280px, calc(var(--main-margin-width) - 2 * var(--gap-size-h))); + + /* Move into the right margin */ + float: right; + clear: right; + /* Center it in the right margin */ + margin-right: calc(-1 * ((var(--main-margin-width) + var(--note-width) + var(--content-padding-x)) / 2)); + /* General margins */ + margin-top: 0.15em; + margin-bottom: 0.8em; + + width: var(--note-width); + + font-size: 0.85em; + color: var(--endnote-fg); + /* Gold-tinted card, works on both light and dark paper */ + background: color-mix(in srgb, var(--gold) 7%, var(--surface-card)); + border: 1px solid color-mix(in srgb, var(--gold) 30%, var(--border)); + border-radius: var(--radius); + padding: 0.4em 0.6em; +} + +/* Reset the backlink sup to baseline, because it looks nicer */ +.sidenote sup[role="doc-backlink"] { + font-size: 1em; + vertical-align: baseline; + margin-right: 0.3em; +} + +/* + Leave out sidenotes for narrow display width or print, still has endnotes + Breakpoint: --main-margin-width ≥ reasonable note width (150px) + 2 * --gap-size-h +*/ +@media (max-width: 1256px) { + .sidenote { + display: none; + } +} + +@media print { + .sidenote { + display: none; + } +} diff --git a/spec/sidenotes.js b/spec/sidenotes.js new file mode 100644 index 000000000..3e4bcbc99 --- /dev/null +++ b/spec/sidenotes.js @@ -0,0 +1,27 @@ +// Progressive enhancement: display footnotes as sidenotes in the right margin. +// If no JS available, stick to the regular endnotes. +// +// Most position is done by CSS (sidenotes.css), we just have to insert an aside +// in the right place. +// +// Loaded by a script tag with defer=true so the iife runs at an okay time +// and we avoid DOMContentLoaded stuff +(() => { + for (const endnote of document.querySelectorAll('section[role="doc-endnotes"] > ol > li')) { + for (const ref of document.querySelectorAll(`sup[role="doc-noteref"] > a[href="#${CSS.escape(endnote.id)}"]`)) { + const sup = ref.parentElement; + const aside = document.createElement("aside"); + aside.className = "sidenote"; + + const content = endnote.cloneNode(true); + aside.replaceChildren(...content.childNodes); + + // Duplicate of the real endnote: keep it out of the tab order and a11y tree + aside.setAttribute("aria-hidden", "true"); + // incomplete selector, but could be extended if anything becomes relevant, ever + aside.querySelectorAll("a, summary, iframe, [tabindex]").forEach(el => el.setAttribute("tabindex", "-1")); + + sup.after(aside); + } + } +})(); diff --git a/spec/sign.typ b/spec/sign.typ index 14a6e4000..2649822ae 100644 --- a/spec/sign.typ +++ b/spec/sign.typ @@ -1,10 +1,8 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": render_chip_variable_table, total_nr_variables, render_chip_assumptions, render_constraint_table, compute_nr_interactions, #let config = load_config() #let chip = load_chip("src/sign.toml", config) -#show: book-page(chip.name) #let nr_variables = total_nr_variables(chip) #let nr_interactions = compute_nr_interactions(chip) diff --git a/spec/signatures.typ b/spec/signatures.typ index 4d0840a66..969cfaaa7 100644 --- a/spec/signatures.typ +++ b/spec/signatures.typ @@ -1,8 +1,5 @@ -#import "/book.typ": book-page #import "/src.typ": load_signatures, load_config -#import "/expr.typ": type_to_code - -#show: book-page("signatures.typ") +#import "/expr.typ": type_to_code, flatten_code #let config = load_config() #let signatures = load_signatures(config) @@ -27,7 +24,7 @@ type_to_code(output) + `; ` } else {``} - return [#cond_str#raw(sig.tag)#lb#output_str#input_str#rb] + return flatten_code([#cond_str#raw(sig.tag)#lb#output_str#input_str#rb]) } // Compute the bus size of an interaction diff --git a/spec/ebook.typ b/spec/spec.typ similarity index 94% rename from spec/ebook.typ rename to spec/spec.typ index 1bd691b9f..b5a6618f2 100644 --- a/spec/ebook.typ +++ b/spec/spec.typ @@ -1,4 +1,4 @@ -#import "/book.typ": meta, common-formatting +#import "/meta.typ": meta, common-formatting #set document(author: meta.authors, title: meta.title) @@ -39,6 +39,6 @@ pagebreak(weak: true) [#heading(level: 2, supplement: [Section], sec_title)#ref] set heading(offset: 2) - include sec + include sec + ".typ" } } diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 6a001e96b..81d42f9f3 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -39,7 +39,7 @@ pad = 0 [[variables.output]] name = "out" type = "DWordWL" -desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" +desc = "$#`in` <<\\/>>\\/>>> (#`shift` mod 32 dot (2 - #`word_instr`))$" pad = 0 # Auxiliary @@ -127,7 +127,7 @@ def = {idx="i", iter=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i [[variables.virtual]] name = "shifted" type = "DWordHL" -desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" +desc = "$#`in` <<\\/>>\\/>>> (#`shift` mod 32 dot (2 - #`word_instr`))$" def = {idx="i", iter=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 4, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} # Multiplicities diff --git a/spec/store.typ b/spec/store.typ index 5b9872b58..284c3be17 100644 --- a/spec/store.typ +++ b/spec/store.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page, rj #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -12,8 +11,6 @@ #let config = load_config() #let chip = load_chip("src/store.toml", config) - -#show: book-page(chip.name) #let store = raw(chip.name) The #store chip provides functionality to store a value to memory. diff --git a/spec/streaming.typ b/spec/streaming.typ index 9f435bd56..18255b3a6 100644 --- a/spec/streaming.typ +++ b/spec/streaming.typ @@ -1,4 +1,3 @@ -#import "/book.typ": book-page #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_assumptions, @@ -9,8 +8,6 @@ total_nr_variables, ) -#show: book-page("streaming.typ") - #let config = load_config() #let l2gchip = load_chip("src/l2g.toml", config) #let l2g = raw(l2gchip.name) diff --git a/spec/style.css b/spec/style.css new file mode 100644 index 000000000..529856033 --- /dev/null +++ b/spec/style.css @@ -0,0 +1,558 @@ +/* Brand colors */ +:root { + --gold: #ffd700; + --gold-hover: #efcb00; + --gold-bronze: #6b5200; + --accent-ink: #1a1a1a; + --logo-field: #0d0d0d; + + --bg: #fbfaf7; + --bg-subtle: #f2f1ed; + --surface-card: #ffffff; + --text: #18181a; + --text-muted: #56565c; + --border: #e6e4dd; + --border-strong: #d7d5cd; + + --link: #6b5200; + --status-error: #b3261e; + --status-ok: #1c7c43; +} +@media (prefers-color-scheme: dark) { + :root { + --gold-hover: #ffe34d; + --bg: #101113; + --bg-subtle: #15161a; + --surface-card: #1a1b1f; + --text: #ededec; + --text-muted: #a2a2a8; + --border: #2a2b30; + --border-strong: #3a3b42; + --link: #ffd700; + --status-error: #f1707a; + --status-ok: #5fcf8e; + } +} + +/* Configuration */ +:root { + --content-max-width: 860px; + --content-padding-x: 48px; + --header-height: 72px; + --border-size: 1px; + --table-header-border-size: 3px; + + --radius: 4px; + + --fg: var(--text); + --author-fg: var(--text-muted); + --endnote-fg: var(--text-muted); + --header-bg: var(--bg-subtle); + --sidebar-bg: var(--bg-subtle); + --sidebar-fg: var(--text); + --code-bg: var(--bg-subtle); + --code-fg: var(--text); + --table-border: var(--text); + --aside-border: var(--border-strong); + --aside-border-size: 2pt; + --link-hover: var(--gold-bronze); + --focus-outline-color: var(--text); + --nav-hover-bg: color-mix(in srgb, var(--gold) 15%, var(--sidebar-bg)); + --nav-current-bg: color-mix(in srgb, var(--gold) 28%, var(--sidebar-bg)); + + /* Try to match typst PDF fonts */ + --font-body: "Libertinus Serif", serif; + --font-code: "DejaVu Sans Mono", monospace; + --font-math: "New Computer Modern Math", "STIX Two Text", math, serif; + --font-mtext: "New Computer Modern Math", "STIX Two Text", serif; + + /* Breakpoints (for reference — CSS vars can't be used in @media) */ + /* --bp-mobile: 768px; */ +} + +@media (prefers-color-scheme: dark) { + :root { + /* Exceptions */ + --link-hover: var(--gold-hover); + --focus-outline-color: var(--gold); + } + + /* Overwrite typst's syntax highlight colors. We've only seen these two emitted so far */ + code span[style="color: #4b69c6"] { color: #82aaff !important; } + code span[style="color: #d73948"] { color: var(--status-error) !important; } +} + +/* Keep fragment targets (footnote backlinks, in-page references) clear of + the sticky header when scrolled to */ +:root { + scroll-padding-top: calc(var(--header-height) + var(--border-size)); +} + + +/* layout things */ +* { + box-sizing: border-box; +} + +html { + font-size: 16px; +} + +body { + margin: 0; + padding: 0; + font-family: var(--font-body); + color: var(--fg); + background: var(--bg); + display: grid; + grid-template: + "noHeader header header" var(--header-height) + "headerBorder headerBorder headerBorder" var(--border-size) + "nav main ." 1fr + "nav footnotes ." auto + "nav footnav footnav" auto + / minmax(139px, 1fr) 6fr 1fr; + /* We go for the minmax to ensure the nav doesn't get squished too much. + 139px is still enough space, and it makes sure we have pure 1fr-6fr-1fr + at the sidenotes.css breakpoint. + The 139 is subtracted before the fr calculations, so we need (width - 139)/8 >= 139. + And so bp >= 9 * 139. + */ + min-height: 100vh; +} + +p:empty { + display: none; +} + +@media (max-width: 768px) { + body { + grid-template: + "header" var(--header-height) + "headerBorder" var(--border-size) + "nav" auto + "main" auto + "footnotes" auto + "footnav" auto; + } + + :root { + --content-padding-x: 16px; + } +} + +/* index page */ +main > h1 { /* title */ + text-align: center; +} + +main > h1 + p { /* authors */ + color: var(--author-fg); + text-align: center; +} + +h1 + p em { /* version */ + display: block; + color: var(--fg); + margin-bottom: 0.2em; +} + +/* nav sidebar */ +nav:not(.prev-next) { + grid-area: nav; + background: var(--sidebar-bg); + border-right: var(--border-size) solid var(--border); + padding: 20px; + overflow-y: auto; + min-height: calc(100vh - var(--header-height) - var(--border-size)); + font-size: 0.9em; + position: sticky; + top: calc(var(--header-height) + var(--border-size)); + max-height: calc(100vh - var(--header-height) - var(--border-size)); +} + +nav ul { + list-style: none; + padding: 0; + margin: 0 0 16px 0; +} + +nav li { + margin: 2px 0; +} + +nav li a { + display: block; + padding: 4px 8px; + border-radius: var(--radius); + color: var(--sidebar-fg); + text-decoration: none; +} + +nav li a:hover { + background: var(--nav-hover-bg); +} + +nav li a.current { + background: var(--nav-current-bg); + box-shadow: inset 3px 0 0 var(--gold); + font-weight: 600; + pointer-events: none; +} + +nav li code { + padding: 0 4px; +} + +.desktop-nav { + display: block; +} + +.mobile-nav { + display: none; +} + +@media (max-width: 768px) { + nav:not(.prev-next) { + height: auto; + min-height: fit-content; + border-right: none; + border-bottom: var(--border-size) solid var(--border); + padding: 0; + z-index: 5; + } + + .desktop-nav { + display: none; + } + + .mobile-nav { + display: block; + } + + .mobile-nav summary { + display: block; + cursor: pointer; + user-select: none; + font-weight: 600; + font-size: 0.9rem; + padding: 10px 20px; + border-bottom: var(--border-size) solid var(--border); + list-style: none; + } + + .mobile-nav summary::before { + content: '\2630 '; + } + + .mobile-nav summary::-webkit-details-marker { + display: none; + } +} + +/* nav footer */ +nav.prev-next { + grid-area: footnav; + display: flex; + justify-content: space-between; + padding: 0.8em var(--content-padding-x); + border-top: var(--border-size) solid var(--border); + background: var(--bg); + position: sticky; + bottom: 0; +} + +nav.prev-next .next { + text-align: right; +} + +nav.prev-next div:not(:has(a)) { + visibility: hidden; +} + +nav.prev-next a { + display: inline-block; + text-decoration: none; + padding: 0.4em 0.8em; + border-radius: var(--radius); + font-size: 0.9em; +} + +nav.prev-next a:hover { + background: var(--nav-hover-bg); + text-decoration: underline; +} + +nav.prev-next .prev a::before { + content: "← "; +} + +nav.prev-next .next a::after { + content: " →"; +} + + +/* Overall title */ +body > header { + grid-area: header; + height: var(--header-height); + padding-top: 20px; + padding-left: var(--content-padding-x); + background: var(--header-bg); + font-size: 1.5em; + margin: 0; + position: sticky; + top: 0; + z-index: 10; + white-space: nowrap; + overflow: hidden; + text-overflow: ellipsis; +} + +body > header h1 { + margin: 0; + font-size: 1em; +} + +body > header a, +body > header a:hover { + color: inherit; + text-decoration: none; +} + +.subheader { + color: var(--author-fg); + font-size: 0.6em; + font-weight: 400; + white-space: nowrap; +} + +.subheader::before { + /* A bullet + some spacing */ + content: " \2022 \00a0"; +} + +body::before { + content: ""; + grid-area: noHeader; + background: var(--header-bg); + position: sticky; + top: 0; + min-height: var(--header-height); + z-index: 1; /* Go above the nav bar */ +} + +body::after { + content: ""; + grid-area: headerBorder; + background: var(--gold); + position: sticky; + top: var(--header-height); +} + +@media (max-width: 768px) { + body::before { + content: none; + } +} + +/* main body */ +main { + grid-area: main; + max-width: var(--content-max-width); + padding: 0 var(--content-padding-x); + margin: 0 auto; + width: 100%; + min-width: 0; +} + +a { + color: var(--link); + text-decoration: none; +} + +a:hover { + color: var(--link-hover); + text-decoration: underline; +} + +:focus-visible { + outline: 3px solid; + outline-color: var(--focus-outline-color); + outline-offset: 2px; + border-radius: var(--radius); +} + +/* highlights */ +figure[data-kind="highlight"] { + margin: 1em 0; + border: var(--aside-border-size) solid var(--aside-border); + border-radius: var(--radius); + overflow-x: auto; + overflow-y: clip; + padding: 0 1em 1em; +} + +figure[data-kind="highlight"] figcaption { + /* Make it stick in case of overflow-x */ + position: sticky; + left: -1em; + + /* Span the entire width */ + margin: 0 -1em 0.5em; + /* Separator between title and body */ + border-bottom: var(--aside-border-size) solid var(--aside-border); + + /* Colors are provided through typst */ + padding: 0.4em 1em; + font-weight: 600; + display: block; + text-align: center; +} + +/* theorem boxes */ +figure:is([data-kind="lemma"], [data-kind="corollary"]) { + border-radius: var(--radius); + overflow-x: auto; + overflow-y: clip; + margin: 1em 0; + padding: 1em; + background-color: var(--bg-subtle); +} + +figure:is([data-kind="lemma"], [data-kind="corollary"]) p:first-child { + margin-top: 0; +} + +figure:is([data-kind="lemma"], [data-kind="corollary"]) p:last-child { + margin-bottom: 0; +} + +figure[data-kind="proof"] math:has(.qed) { + float: right; +} + +figure[data-kind="proof"] math:has(.qed)::before { + content: "∎" +} + +/* footnotes */ +section[role="doc-endnotes"] { + grid-area: footnotes; + max-width: var(--content-max-width); + margin: 0 auto; + width: 100%; + padding: 2em var(--content-padding-x) 1em; + border-top: var(--border-size) solid var(--border); + font-size: 0.85em; + color: var(--endnote-fg); +} + +section[role="doc-endnotes"] ol { + padding: 0; + margin: 0; +} + +section[role="doc-endnotes"] li { + padding: 4px 0 4px 1.8em; + text-indent: -1.8em; + list-style: none; +} + +section[role="doc-endnotes"] li sup[role="doc-backlink"] { + margin-right: 0.3em; +} + +section[role="doc-endnotes"]:has(ol:empty) { + display: none; +} + +sup[role="doc-noteref"] { + font-size: 0.6em; + vertical-align: text-top; +} + +/* code blocks */ +code { + font-family: var(--font-code); + font-size: 0.7rem; + color: var(--code-fg); + background: var(--code-bg); + padding: 2px 4px; + border-radius: var(--radius); +} + +h1 code, h2 code { + font-size: 1rem; +} + +pre { + background: var(--code-bg); + border: var(--border-size) solid var(--border); + border-radius: var(--radius); + padding: 12px 16px; + overflow-x: auto; + overflow-y: clip; +} + +pre code { + background: none; + padding: 0; + border-radius: 0; +} + +/* tables */ +figure { + margin: 1em 0.3em; + overflow-x: auto; + overflow-y: clip; +} + +table { + border-collapse: collapse; + width: 100%; +} + +thead tr:first-child { + border-bottom: var(--table-header-border-size) solid var(--table-border); +} + +tfoot tr:first-child { + border-top: var(--table-header-border-size) solid var(--table-border); +} + +tr:has(th em) { + border-bottom: var(--border-size) solid var(--table-border); + text-align: left; +} + +tr th:has(em) { + border-bottom: var(--border-size) solid var(--table-border); + font-weight: normal; +} + +tbody tr th:has(em) { + padding-top: 1.5em; +} + +.striped table tbody tr:nth-child(odd) { + background: color-mix(in srgb, var(--gold) 10%, var(--bg)); +} + +/* math */ +math { + font-family: var(--font-math); +} + +math[display="block"] { + display: block; + text-align: center; + font-size: 1.12em; + margin: 1.2em 0; + overflow-x: auto; + overflow-y: clip; +} + +mtext { + font-family: var(--font-mtext); +} diff --git a/spec/templates/page.typ b/spec/templates/page.typ deleted file mode 100644 index 4ec7b27ac..000000000 --- a/spec/templates/page.typ +++ /dev/null @@ -1,167 +0,0 @@ -// This is important for shiroa to produce a responsive layout -// and multiple targets. -#import "@preview/shiroa:0.3.1": ( - get-page-width, is-html-target, is-pdf-target, is-web-target, plain-text, shiroa-sys-target, templates, -) -#import templates: * - -/// The site theme to use. If we renders to static HTML, it is suggested to use `starlight`. -/// otherwise, since `starlight` with dynamic SVG HTML is not supported, `mdbook` is used. -/// The `is-html-target(exclude-wrapper: true)` is currently a bit internal so you shouldn't use it other place. -#let web-theme = if is-html-target(exclude-wrapper: true) { "starlight" } else { "mdbook" } -#let is-starlight-theme = web-theme == "starlight" - -// Metadata -#let page-width = get-page-width() -#let is-html-target = is-html-target() -#let is-pdf-target = is-pdf-target() -#let is-web-target = is-web-target() -#let sys-is-html-target = ("target" in dictionary(std)) - -// Theme (Colors) -#let themes = theme-box-styles-from(toml("theme-style.toml"), read: it => read(it)) -#let ( - default-theme: ( - style: theme-style, - is-dark: is-dark-theme, - is-light: is-light-theme, - main-color: main-color, - dash-color: dash-color, - code-extra-colors: code-extra-colors, - ), -) = themes; -#let ( - default-theme: default-theme, -) = themes; -#let theme-box = theme-box.with(themes: themes) - -// Fonts -#let main-font = ( - // "Charter", - // "Source Han Serif SC", - // "Source Han Serif TC", - // shiroa's embedded font - "Libertinus Serif", -) -#let code-font = ( - // "BlexMono Nerd Font Mono", - // shiroa's embedded font - "DejaVu Sans Mono", -) - -// Sizes -#let main-size = if is-web-target { - 16pt -} else { - 10.5pt -} -#let heading-sizes = if is-web-target { - (2, 1.5, 1.17, 1, 0.83).map(it => it * main-size) -} else { - (26pt, 22pt, 14pt, 12pt, main-size) -} -#let list-indent = 0.5em - -// Put your custom CSS here. -#let extra-css = ```css -.site-title { - font-size: 1.2rem; - font-weight: 600; - font-style: italic; -} -``` - -/// The project show rule that is used by all pages. -/// -/// Example: -/// ```typ -/// #show: project -/// ``` -/// -/// - title (str): The title of the page. -/// - description (auto): The description of the page. -/// - If description is `auto`, it will be generated from the plain body. -/// - If description is `none`, an error is raised to force migration. In future, `none` will mean the description is not generated. -/// - 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 - set document( - author: authors, - title: title, - ) if not is-pdf-target - - // set web/pdf page properties - set page( - numbering: none, - number-align: center, - width: page-width, - ) if not (sys-is-html-target or is-html-target) - - // remove margins for web target - set page( - margin: ( - // reserved beautiful top margin - top: 20pt, - // reserved for our heading style. - // If you apply a different heading style, you may remove it. - left: 20pt, - // Typst is setting the page's bottom to the baseline of the last line of text. So bad :(. - bottom: 0.5em, - // remove rest margins. - rest: 0pt, - ), - height: auto, - ) if is-web-target and not is-html-target - - let common = ( - web-theme: web-theme, - ) - - show: template-rules.with( - book-meta: include "/book.typ", - title: title, - description: description, - plain-body: plain-body, - extra-assets: (extra-css,), - ..common, - ) - - // Set main text - set text( - font: main-font, - size: main-size, - fill: main-color, - lang: "en", - ) - - 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/templates/theme-style.toml b/spec/templates/theme-style.toml deleted file mode 100644 index 128d0b171..000000000 --- a/spec/templates/theme-style.toml +++ /dev/null @@ -1,30 +0,0 @@ - -[light] -color-scheme = "light" -main-color = "#000" -dash-color = "#20609f" -code-theme = "" - -[rust] -color-scheme = "light" -main-color = "#262625" -dash-color = "#2b79a2" -code-theme = "" - -[coal] -color-scheme = "dark" -main-color = "#98a3ad" -dash-color = "#2b79a2" -code-theme = "tokyo-night.tmTheme" - -[navy] -color-scheme = "dark" -main-color = "#bcbdd0" -dash-color = "#2b79a2" -code-theme = "tokyo-night.tmTheme" - -[ayu] -color-scheme = "dark" -main-color = "#c5c5c5" -dash-color = "#0096cf" -code-theme = "tokyo-night.tmTheme" diff --git a/spec/templates/tokyo-night.tmTheme b/spec/templates/tokyo-night.tmTheme deleted file mode 100644 index 24829e7c4..000000000 --- a/spec/templates/tokyo-night.tmTheme +++ /dev/null @@ -1,1308 +0,0 @@ - - - - - name - Tokyo Night - settings - - - settings - - caret - #c0caf5 - selection - #515c7e4d - lineHighlight - #1e202e - foreground - #a9b1d6 - background - #1a1b26 - invisibles - #363b54 - - - - name - Italics - Comments, Storage, Keyword Flow, Vue attributes, Decorators - scope - comment,meta.var.expr storage.type,keyword.control.flow,keyword.control.return,meta.directive.vue punctuation.separator.key-value.html,meta.directive.vue entity.other.attribute-name.html,tag.decorator.js entity.name.tag.js,tag.decorator.js punctuation.definition.tag.js,storage.modifier - settings - - fontStyle - italic - - - - name - Fix YAML block scalar - scope - keyword.control.flow.block-scalar.literal - settings - - fontStyle - - - - - name - Comment - scope - comment,comment.block.documentation,punctuation.definition.comment,comment.block.documentation punctuation - settings - - foreground - #444b6a - - - - name - Comment Doc - scope - keyword.operator.assignment.jsdoc,comment.block.documentation variable,comment.block.documentation storage,comment.block.documentation keyword,comment.block.documentation support,comment.block.documentation markup,comment.block.documentation markup.inline.raw.string.markdown,meta.other.type.phpdoc.php keyword.other.type.php,meta.other.type.phpdoc.php support.other.namespace.php,meta.other.type.phpdoc.php punctuation.separator.inheritance.php,meta.other.type.phpdoc.php support.class,keyword.other.phpdoc.php,log.date - settings - - foreground - #5a638c - - - - name - Comment Doc Emphasized - scope - meta.other.type.phpdoc.php support.class,comment.block.documentation storage.type,comment.block.documentation punctuation.definition.block.tag,comment.block.documentation entity.name.type.instance - settings - - foreground - #646e9c - - - - name - Number, Boolean, Undefined, Null - scope - variable.other.constant,punctuation.definition.constant,constant.language,constant.numeric,support.constant - settings - - foreground - #ff9e64 - - - - name - String, Symbols - scope - string,constant.other.symbol,constant.other.key,meta.attribute-selector - settings - - fontStyle - - foreground - #9ece6a - - - - name - Colors - scope - constant.other.color,constant.other.color.rgb-value.hex punctuation.definition.constant - settings - - foreground - #9aa5ce - - - - name - Invalid - scope - invalid,invalid.illegal - settings - - foreground - #ff5370 - - - - name - Invalid deprecated - scope - invalid.deprecated - settings - - foreground - #bb9af7 - - - - name - Storage Type - scope - storage.type - settings - - foreground - #bb9af7 - - - - name - Storage - modifier, var, const, let - scope - meta.var.expr storage.type,storage.modifier - settings - - foreground - #9d7cd8 - - - - name - Interpolation, PHP tags, Smarty tags - scope - punctuation.definition.template-expression,punctuation.section.embedded,meta.embedded.line.tag.smarty,support.constant.handlebars,punctuation.section.tag.twig - settings - - foreground - #7dcfff - - - - name - Blade, Twig, Smarty Handlebars keywords - scope - keyword.control.smarty,keyword.control.twig,support.constant.handlebars keyword.control,keyword.operator.comparison.twig,keyword.blade,entity.name.function.blade - settings - - foreground - #0db9d7 - - - - name - Spread - scope - keyword.operator.spread,keyword.operator.rest - settings - - foreground - #f7768e - fontStyle - bold - - - - name - Operator, Misc - scope - keyword.operator,keyword.control.as,keyword.other,keyword.operator.bitwise.shift,punctuation,expression.embbeded.vue punctuation.definition.tag,text.html.twig meta.tag.inline.any.html,meta.tag.template.value.twig meta.function.arguments.twig,meta.directive.vue punctuation.separator.key-value.html,punctuation.definition.constant.markdown,punctuation.definition.string,punctuation.support.type.property-name,text.html.vue-html meta.tag,meta.attribute.directive,punctuation.definition.keyword,punctuation.terminator.rule,punctuation.definition.entity,punctuation.separator.inheritance.php,keyword.other.template,keyword.other.substitution,entity.name.operator,meta.property-list punctuation.separator.key-value,meta.at-rule.mixin punctuation.separator.key-value,meta.at-rule.function variable.parameter.url - settings - - foreground - #89ddff - - - - name - Import, Export, From, Default - scope - keyword.control.import,keyword.control.export,keyword.control.from,keyword.control.default,meta.import keyword.other - settings - - foreground - #7dcfff - - - - name - Keyword - scope - keyword,keyword.control,keyword.other.important - settings - - foreground - #bb9af7 - - - - name - Keyword SQL - scope - keyword.other.DML - settings - - foreground - #7dcfff - - - - name - Keyword Operator Logical, Arrow, Ternary, Comparison - scope - keyword.operator.logical,storage.type.function,keyword.operator.bitwise,keyword.operator.ternary,keyword.operator.comparison,keyword.operator.relational,keyword.operator.or.regexp - settings - - foreground - #bb9af7 - - - - name - Tag - scope - entity.name.tag - settings - - foreground - #f7768e - - - - name - Tag - Custom - scope - entity.name.tag support.class.component,meta.tag.custom entity.name.tag,meta.tag - settings - - foreground - #de5971 - - - - name - Tag Punctuation - scope - punctuation.definition.tag - settings - - foreground - #ba3c97 - - - - name - Globals, PHP Constants, etc - scope - constant.other.php,variable.other.global.safer,variable.other.global.safer punctuation.definition.variable,variable.other.global,variable.other.global punctuation.definition.variable,constant.other - settings - - foreground - #e0af68 - - - - name - Variables - scope - variable,support.variable,string constant.other.placeholder,variable.parameter.handlebars,variable.other.object - settings - - foreground - #c0caf5 - - - - name - Variable Array Key - scope - meta.array.literal variable - settings - - foreground - #7dcfff - - - - name - Object Key - scope - meta.object-literal.key,entity.name.type.hcl,string.alias.graphql,string.unquoted.graphql,string.unquoted.alias.graphql,meta.group.braces.curly constant.other.object.key.js string.unquoted.label.js,meta.field.declaration.ts variable.object.property,meta.block entity.name.label - settings - - foreground - #73daca - - - - name - Object Property - scope - variable.other.property,support.variable.property,support.variable.property.dom,meta.function-call variable.other.object.property - settings - - foreground - #7dcfff - - - - name - Object Property - scope - variable.other.object.property - settings - - foreground - #c0caf5 - - - - name - Object Literal Member lvl 3 (Vue Prop Validation) - scope - meta.objectliteral meta.object.member meta.objectliteral meta.object.member meta.objectliteral meta.object.member meta.object-literal.key - settings - - foreground - #41a6b5 - - - - name - C-related Block Level Variables - scope - source.cpp meta.block variable.other - settings - - foreground - #f7768e - - - - name - Other Variable - scope - support.other.variable - settings - - foreground - #f7768e - - - - name - Methods - scope - meta.class-method.js entity.name.function.js,entity.name.method.js,variable.function.constructor,keyword.other.special-method,storage.type.cs - settings - - foreground - #7aa2f7 - - - - name - Function Definition - scope - entity.name.function,variable.other.enummember,meta.function-call,meta.function-call entity.name.function,variable.function,meta.definition.method entity.name.function,meta.object-literal entity.name.function - settings - - foreground - #7aa2f7 - - - - name - Function Argument - scope - variable.parameter.function.language.special,variable.parameter,meta.function.parameters punctuation.definition.variable,meta.function.parameter variable - settings - - foreground - #e0af68 - - - - name - Constant, Tag Attribute - scope - keyword.other.type.php,storage.type.php,constant.character,constant.escape,keyword.other.unit - settings - - foreground - #bb9af7 - - - - name - Variable Definition - scope - meta.definition.variable variable.other.constant,meta.definition.variable variable.other.readwrite,variable.declaration.hcl variable.other.readwrite.hcl,meta.mapping.key.hcl variable.other.readwrite.hcl,variable.other.declaration - settings - - foreground - #bb9af7 - - - - name - Inherited Class - scope - entity.other.inherited-class - settings - - fontStyle - - foreground - #bb9af7 - - - - name - Class, Support, DOM, etc - scope - support.class,support.type,variable.other.readwrite.alias,support.orther.namespace.use.php,meta.use.php,support.other.namespace.php,support.type.sys-types,support.variable.dom,support.constant.math,support.type.object.module,support.constant.json,entity.name.namespace,meta.import.qualifier,variable.other.constant.object - settings - - foreground - #0db9d7 - - - - name - Class Name - scope - entity.name - settings - - foreground - #c0caf5 - - - - name - Support Function - scope - support.function - settings - - foreground - #0db9d7 - - - - name - CSS Class and Support - scope - source.css support.type.property-name,source.sass support.type.property-name,source.scss support.type.property-name,source.less support.type.property-name,source.stylus support.type.property-name,source.postcss support.type.property-name,support.type.property-name.css,support.type.vendored.property-name,support.type.map.key - settings - - foreground - #7aa2f7 - - - - name - CSS Font - scope - support.constant.font-name,meta.definition.variable - settings - - foreground - #9ece6a - - - - name - CSS Class - scope - entity.other.attribute-name.class,meta.at-rule.mixin.scss entity.name.function.scss - settings - - foreground - #9ece6a - - - - name - CSS ID - scope - entity.other.attribute-name.id - settings - - foreground - #fc7b7b - - - - name - CSS Tag - scope - entity.name.tag.css - settings - - foreground - #0db9d7 - - - - name - CSS Tag Reference, Pseudo & Class Punctuation - scope - entity.other.attribute-name.pseudo-class punctuation.definition.entity,entity.other.attribute-name.pseudo-element punctuation.definition.entity,entity.other.attribute-name.class punctuation.definition.entity,entity.name.tag.reference - settings - - foreground - #e0af68 - - - - name - CSS Punctuation - scope - meta.property-list - settings - - foreground - #9abdf5 - - - - name - CSS at-rule fix - scope - meta.property-list meta.at-rule.if,meta.at-rule.return variable.parameter.url,meta.property-list meta.at-rule.else - settings - - foreground - #ff9e64 - - - - name - CSS Parent Selector Entity - scope - entity.other.attribute-name.parent-selector-suffix punctuation.definition.entity.css - settings - - foreground - #73daca - - - - name - CSS Punctuation comma fix - scope - meta.property-list meta.property-list - settings - - foreground - #9abdf5 - - - - name - SCSS @ - scope - meta.at-rule.mixin keyword.control.at-rule.mixin,meta.at-rule.include entity.name.function.scss,meta.at-rule.include keyword.control.at-rule.include - settings - - foreground - #bb9af7 - - - - name - SCSS Mixins, Extends, Include Keyword - scope - keyword.control.at-rule.include punctuation.definition.keyword,keyword.control.at-rule.mixin punctuation.definition.keyword,meta.at-rule.include keyword.control.at-rule.include,keyword.control.at-rule.extend punctuation.definition.keyword,meta.at-rule.extend keyword.control.at-rule.extend,entity.other.attribute-name.placeholder.css punctuation.definition.entity.css,meta.at-rule.media keyword.control.at-rule.media,meta.at-rule.mixin keyword.control.at-rule.mixin,meta.at-rule.function keyword.control.at-rule.function,keyword.control punctuation.definition.keyword - settings - - foreground - #9d7cd8 - - - - name - SCSS Include Mixin Argument - scope - meta.property-list meta.at-rule.include - settings - - foreground - #c0caf5 - - - - name - CSS value - scope - support.constant.property-value - settings - - foreground - #ff9e64 - - - - name - Sub-methods - scope - entity.name.module.js,variable.import.parameter.js,variable.other.class.js - settings - - foreground - #c0caf5 - - - - name - Language methods - scope - variable.language - settings - - foreground - #f7768e - - - - name - Variable punctuation - scope - variable.other punctuation.definition.variable - settings - - foreground - #c0caf5 - - - - name - Keyword this with Punctuation, ES7 Bind Operator - scope - source.js constant.other.object.key.js string.unquoted.label.js,variable.language.this punctuation.definition.variable,keyword.other.this - settings - - foreground - #f7768e - - - - name - HTML Attributes - scope - entity.other.attribute-name,text.html.basic entity.other.attribute-name.html,text.html.basic entity.other.attribute-name - settings - - foreground - #bb9af7 - - - - name - HTML Character Entity - scope - text.html constant.character.entity - settings - - foreground - #0DB9D7 - - - - name - Vue (Vetur / deprecated) Template attributes - scope - entity.other.attribute-name.id.html,meta.directive.vue entity.other.attribute-name.html - settings - - foreground - #bb9af7 - - - - name - CSS ID's - scope - source.sass keyword.control - settings - - foreground - #7aa2f7 - - - - name - CSS psuedo selectors - scope - entity.other.attribute-name.pseudo-class,entity.other.attribute-name.pseudo-element,entity.other.attribute-name.placeholder,meta.property-list meta.property-value - settings - - foreground - #bb9af7 - - - - name - Inserted - scope - markup.inserted - settings - - foreground - #449dab - - - - name - Deleted - scope - markup.deleted - settings - - foreground - #914c54 - - - - name - Changed - scope - markup.changed - settings - - foreground - #6183bb - - - - name - Regular Expressions - scope - string.regexp - settings - - foreground - #b4f9f8 - - - - name - Regular Expressions - Punctuation - scope - punctuation.definition.group - settings - - foreground - #f7768e - - - - name - Regular Expressions - Character Class - scope - constant.other.character-class.regexp - settings - - foreground - #bb9af7 - - - - name - Regular Expressions - Character Class Set - scope - constant.other.character-class.set.regexp,punctuation.definition.character-class.regexp - settings - - foreground - #e0af68 - - - - name - Regular Expressions - Quantifier - scope - keyword.operator.quantifier.regexp - settings - - foreground - #89ddff - - - - name - Regular Expressions - Backslash - scope - constant.character.escape.backslash - settings - - foreground - #c0caf5 - - - - name - Escape Characters - scope - constant.character.escape - settings - - foreground - #89ddff - - - - name - Decorators - scope - tag.decorator.js entity.name.tag.js,tag.decorator.js punctuation.definition.tag.js - settings - - foreground - #7aa2f7 - - - - name - CSS Units - scope - keyword.other.unit - settings - - foreground - #f7768e - - - - name - JSON Key - Level 0 - scope - source.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #7aa2f7 - - - - name - JSON Key - Level 1 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #0db9d7 - - - - name - JSON Key - Level 2 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #7dcfff - - - - name - JSON Key - Level 3 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #bb9af7 - - - - name - JSON Key - Level 4 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #e0af68 - - - - name - JSON Key - Level 5 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #0db9d7 - - - - name - JSON Key - Level 6 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #73daca - - - - name - JSON Key - Level 7 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #f7768e - - - - name - JSON Key - Level 8 - scope - source.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json meta.structure.dictionary.value.json meta.structure.dictionary.json support.type.property-name.json - settings - - foreground - #9ece6a - - - - name - Plain Punctuation - scope - punctuation.definition.list_item.markdown - settings - - foreground - #9abdf5 - - - - name - Block Punctuation - scope - meta.block,meta.brace,punctuation.definition.block,punctuation.definition.use,punctuation.definition.class,punctuation.definition.begin.bracket,punctuation.definition.end.bracket,punctuation.definition.switch-expression.begin.bracket,punctuation.definition.switch-expression.end.bracket,punctuation.definition.section.switch-block.begin.bracket,punctuation.definition.section.switch-block.end.bracket,punctuation.definition.group.shell,punctuation.definition.parameters,punctuation.definition.arguments,punctuation.definition.dictionary,punctuation.definition.array,punctuation.section - settings - - foreground - #9abdf5 - - - - name - Markdown - Plain - scope - meta.jsx.children,meta.embedded.block - settings - - foreground - #c0caf5 - - - - name - HTML text - scope - text.html,text.log - settings - - foreground - #9aa5ce - - - - name - Markdown - Markup Raw Inline - scope - text.html.markdown markup.inline.raw.markdown - settings - - foreground - #bb9af7 - - - - name - Markdown - Markup Raw Inline Punctuation - scope - text.html.markdown markup.inline.raw.markdown punctuation.definition.raw.markdown - settings - - foreground - #4E5579 - - - - name - Markdown - Heading 1 - scope - heading.1.markdown entity.name,heading.1.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #89ddff - - - - name - Markdown - Heading 2 - scope - heading.2.markdown entity.name,heading.2.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #61bdf2 - - - - name - Markdown - Heading 3 - scope - heading.3.markdown entity.name,heading.3.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #7aa2f7 - - - - name - Markdown - Heading 4 - scope - heading.4.markdown entity.name,heading.4.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #6d91de - - - - name - Markdown - Heading 5 - scope - heading.5.markdown entity.name,heading.5.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #9aa5ce - - - - name - Markdown - Heading 6 - scope - heading.6.markdown entity.name,heading.6.markdown punctuation.definition.heading.markdown - settings - - fontStyle - bold - foreground - #747ca1 - - - - name - Markup - Italic - scope - markup.italic,markup.italic punctuation - settings - - fontStyle - italic - foreground - #c0caf5 - - - - name - Markup - Bold - scope - markup.bold,markup.bold punctuation - settings - - fontStyle - bold - foreground - #c0caf5 - - - - name - Markup - Bold-Italic - scope - markup.bold markup.italic,markup.bold markup.italic punctuation - settings - - fontStyle - bold italic - foreground - #c0caf5 - - - - name - Markup - Underline - scope - markup.underline,markup.underline punctuation - settings - - fontStyle - underline - - - - name - Markdown - Blockquote - scope - markup.quote punctuation.definition.blockquote.markdown - settings - - foreground - #4e5579 - - - - name - Markup - Quote - scope - markup.quote - settings - - fontStyle - italic - - - - name - Markdown - Link - scope - string.other.link,markup.underline.link,constant.other.reference.link.markdown,string.other.link.description.title.markdown - settings - - foreground - #73daca - - - - name - Markdown - Fenced Code Block - scope - markup.fenced_code.block.markdown,markup.inline.raw.string.markdown,variable.language.fenced.markdown - settings - - foreground - #89ddff - - - - name - Markdown - Separator - scope - meta.separator - settings - - fontStyle - bold - foreground - #444b6a - - - - name - Markup - Table - scope - markup.table - settings - - foreground - #c0cefc - - - - name - Token - Info - scope - token.info-token - settings - - foreground - #0db9d7 - - - - name - Token - Warn - scope - token.warn-token - settings - - foreground - #ffdb69 - - - - name - Token - Error - scope - token.error-token - settings - - foreground - #db4b4b - - - - name - Token - Debug - scope - token.debug-token - settings - - foreground - #b267e6 - - - - name - Apache Tag - scope - entity.tag.apacheconf - settings - - foreground - #f7768e - - - - name - Preprocessor - scope - meta.preprocessor - settings - - foreground - #73daca - - - - name - ENV value - scope - source.env - settings - - foreground - #7aa2f7 - - - - - diff --git a/spec/variables.typ b/spec/variables.typ index d62fec7ac..ecfa83ce6 100644 --- a/spec/variables.typ +++ b/spec/variables.typ @@ -1,8 +1,5 @@ -#import "/book.typ": book-page #import "/src.typ": load_config -#show: book-page("variables.typ") - #let config = load_config() 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.