Skip to content
Open
Show file tree
Hide file tree
Changes from 20 commits
Commits
Show all changes
30 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
cf18f03
subdirectories for assets and chapters
RobinJadoul Aug 26, 2026
76cdf9f
code and lemma background
RobinJadoul Aug 26, 2026
9ff55b9
font size
RobinJadoul Aug 26, 2026
7c17dfe
Space after mobile nav hamburger
RobinJadoul Aug 26, 2026
7609098
Better table column widths
RobinJadoul Aug 26, 2026
aa11bf1
Styling for definition lists
RobinJadoul Aug 26, 2026
7c22f0f
Some more TODOs
RobinJadoul Aug 26, 2026
4f8001e
Update spec/assets/style.css
RobinJadoul Aug 27, 2026
ee2bfca
Manual theme toggle on top of system default
RobinJadoul Aug 28, 2026
6096ac6
Add todo item re emoji fonts
RobinJadoul Sep 3, 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