Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
a44430e
Experimental switch from shiroa to typst html bundle export
RobinJadoul Jun 22, 2026
dccbb12
CSS and general visual improvements for the bundle export
RobinJadoul Jun 25, 2026
2d60346
fix border gap left on mobile
RobinJadoul Jun 25, 2026
44d0055
minor styling
RobinJadoul Jun 25, 2026
0594b32
Sidenotes as progressive enhancement
RobinJadoul Aug 18, 2026
8c0e026
Remove sidenotes from a11y tree and tabstops without killing the links
RobinJadoul Aug 18, 2026
d3105ba
Asides
RobinJadoul Aug 18, 2026
2c62796
Striped table rows for decode
RobinJadoul Aug 19, 2026
24a1f9c
Mark current page in nav as current page for a11y too
RobinJadoul Aug 19, 2026
fdfee15
Move nav after main in html order for nicer tab order
RobinJadoul Aug 19, 2026
2b74419
Responsiveness work
RobinJadoul Aug 19, 2026
7b85eda
Add chapter title to the header bar
RobinJadoul Aug 19, 2026
01dd856
Fonts
RobinJadoul Aug 20, 2026
ad7ad58
accessilibity: role on prev/next nav buttons, put the title in a <hea…
RobinJadoul Aug 20, 2026
6e070cf
Merge spec/main into spec/typst-bundle and solve some of the most obv…
RobinJadoul Aug 21, 2026
c5be459
Merge branch 'spec/main' into spec/typst-bundle
RobinJadoul Aug 21, 2026
8014fbd
Update colors for 3MI brand and design guidelines
RobinJadoul Aug 21, 2026
facfdfc
Make theorem boxes better and eliminate warnings
RobinJadoul Aug 21, 2026
3542ab5
lemma whitespace improvements
RobinJadoul Aug 21, 2026
f980015
Rewrite limbs corollary so that alignment works in both pdf and web
RobinJadoul Aug 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions spec/.gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
dist/*
interaction_count.json
ebook.pdf
bundle/*
spec.pdf
venv/*
16 changes: 8 additions & 8 deletions spec/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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/`.
4 changes: 1 addition & 3 deletions spec/about_ecalls.typ
Original file line number Diff line number Diff line change
@@ -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,
Expand All @@ -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:
Expand Down
4 changes: 1 addition & 3 deletions spec/add.typ
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
#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,

#let config = load_config()
#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)

Expand Down
3 changes: 0 additions & 3 deletions spec/bitwise.typ
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
#import "/book.typ": book-page, rj
#import "/src.typ": load_config, load_chip
#import "/chip.typ": (
render_chip_assumptions,
Expand All @@ -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
Expand Down
230 changes: 0 additions & 230 deletions spec/book.typ

This file was deleted.

3 changes: 0 additions & 3 deletions spec/branch.typ
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
#import "/book.typ": book-page, rj
#import "/src.typ": load_config, load_chip
#import "/chip.typ": (
render_chip_assumptions,
Expand All @@ -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.
Expand Down
27 changes: 0 additions & 27 deletions spec/build_shiroa.sh

This file was deleted.

Loading
Loading