Skip to content

Commit 62ce50e

Browse files
authored
Merge branch 'main' into feat/scaling-improvements
2 parents 00d4ec4 + 7b42e51 commit 62ce50e

57 files changed

Lines changed: 9615 additions & 0 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/workflows/pr_spec.yaml

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
name: Spec tests
2+
on:
3+
pull_request:
4+
branches:
5+
- main
6+
- 'spec/**'
7+
push:
8+
branches: ["**"]
9+
paths: ["spec/**"]
10+
11+
permissions:
12+
contents: read
13+
14+
concurrency:
15+
group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
16+
cancel-in-progress: true
17+
18+
jobs:
19+
spec_structure:
20+
name: Spec structure test
21+
runs-on: ubuntu-latest
22+
steps:
23+
- uses: actions/checkout@v6
24+
- uses: actions/setup-python@v6
25+
- run: python3 spec/tooling/chip.py spec/src/config.toml spec/src/signatures.toml spec/src/*.toml

spec/.editorconfig

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
root = true
2+
3+
[*]
4+
end_of_line = lf
5+
insert_final_newline = true
6+
charset = utf-8
7+
8+
[*.typ]
9+
indent_style = space
10+
indent_size = 2

spec/.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
dist/*
2+
ebook.pdf

spec/README.md

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
# LambdaVM specification
2+
This repository contains specification for [`LambdaVM`](https://github.com/yetanotherco/lambda_vm).
3+
The specification is written in [`Typst`](https://typst.app/) and can be rendered by [`shiroa`](https://myriad-dreamin.github.io/shiroa/) as either a file (pdf) or a wiki (html).
4+
5+
## Installation & Development setup
6+
1. [Install `Typst`](https://github.com/typst/typst?tab=readme-ov-file#installation).
7+
2. [Install `shiroa`](https://myriad-dreamin.github.io/shiroa/guide/installation.html).
8+
3. Clone this repository.
9+
4. Open the repository in a terminal and execute `shiroa serve`.
10+
11+
At this point, the wiki version is hosted locally and is actively updated as you modify the specification files.

spec/about_ecalls.typ

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#import "/book.typ": book-page, aside
2+
#import "/src.typ": load_config, load_chip
3+
#import "/chip.typ": (
4+
render_chip_variable_table,
5+
total_nr_variables,
6+
total_nr_instantiated_columns,
7+
render_constraint_table,
8+
render_chip_assumptions,
9+
render_chip_padding_table,
10+
)
11+
12+
#let config = load_config()
13+
14+
#show: book-page("about_ecalls.typ")
15+
16+
ECALLs provide system-level functionalities to the guest program.
17+
18+
When `ECALL` is executed, it is assumed that:
19+
- register `A7` contains the system call number
20+
#footnote([The RISC-V system call ABI; libriscv.no, #link("https://web.archive.org/web/20260128152107/https://libriscv.no/docs/concepts/syscalls/#the-risc-v-system-call-abi")[[src]]]),
21+
- the arguments are located in registers `A0`-`A6`, and
22+
- the return value is written to `A0`,
23+
where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
24+
#footnote([RISC-V - Register sets; en.wikipedia.org, #link("https://web.archive.org/web/20260209053447/https://en.wikipedia.org/wiki/RISC-V#Register_sets")[[src]]]).

spec/add.typ

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
#import "/book.typ": book-page, et
2+
#import "/src.typ": load_config, load_chip
3+
#import "/chip.typ": render_chip_variable_table, render_chip_assumptions, render_constraint_table, set_nr_interactions, compute_nr_interactions,
4+
5+
#let config = load_config()
6+
#let chip = load_chip("src/add.toml", config)
7+
8+
#show: book-page(chip.name)
9+
10+
#set_nr_interactions(chip, name: "SUB")
11+
#let nr_interactions = compute_nr_interactions(chip)
12+
13+
#let add = raw(chip.name)
14+
#let sub = raw("SUB")
15+
16+
#add is a constraint template that is used to assert that $#`sum` equiv #`lhs` + #`rhs` (mod 2^64)$, under the condition that `cond` is non-zero.
17+
For ease of notation, we moreover introduce the #sub constraint template
18+
$
19+
#`SUB<diff; lhs, rhs>` := #`ADD<lhs; rhs, diff>`,
20+
$
21+
in both conditional and unconditional versions.
22+
It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero.
23+
24+
= Variables
25+
This template introduces #nr_interactions interaction(s).
26+
#render_chip_variable_table(chip, config)
27+
28+
= Assumptions
29+
#render_chip_assumptions(chip, config)
30+
31+
= Constraints
32+
This template introduces the following constraints
33+
#render_constraint_table(chip, config)

spec/bitwise.typ

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
#import "/book.typ": book-page, rj
2+
#import "/src.typ": load_config, load_chip
3+
#import "/chip.typ": (
4+
render_chip_assumptions,
5+
render_chip_variable_table,
6+
total_nr_variables,
7+
total_nr_instantiated_columns,
8+
render_constraint_table,
9+
)
10+
11+
#let config = load_config()
12+
#let chip = load_chip("src/bitwise.toml", config)
13+
14+
#let bitwise = raw(chip.name)
15+
16+
#show: book-page(chip.name)
17+
#let bitwise = raw(chip.name)
18+
19+
The #bitwise chips deal with precomputed lookup tables for bitwise boolean operations
20+
and convenience functionalities over small domains.
21+
22+
= Variables
23+
#let nr_variables = total_nr_variables(chip)
24+
#let nr_columns = total_nr_instantiated_columns(chip, config)
25+
#let nr_precomputed = ("input", "output").map(c => chip.variables.at(c)).flatten().len()
26+
27+
The #bitwise chip is comprised of #nr_variables variables that are expressed using #nr_columns columns.
28+
Of these, the _input_ and _output_ variables (#nr_precomputed in total) are precomputed.
29+
#render_chip_variable_table(chip, config)
30+
31+
*Note*: This table contains one row for every possible value of `(X, Y, Z)`.
32+
As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$.
33+
34+
= Lookup
35+
This chip adds the following interactions to the lookup:
36+
#render_constraint_table(chip, config)
37+
38+
= Notes/Optimizations
39+
The following ideas may prove to be optimizations for the #bitwise chip:
40+
+ Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once.
41+
When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`.
42+
+ Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8<X> := MSB16[256X]`.
43+
Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`).
44+
This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check.
45+
+ Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, etc.) and 20-bit (`HWSL`, `IS_B20`, `ZERO`) lookups in separate tables.

spec/book.typ

Lines changed: 185 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
#import "@preview/shiroa:0.3.1": *
2+
#import "/templates/page.typ": project
3+
4+
#show: book
5+
6+
#let meta = (
7+
title: "Lambda VM specification",
8+
authors: ("3MI Labs", "Aligned"),
9+
version: "0.2",
10+
summary: (
11+
("PROOF SYSTEM", (
12+
("logup.typ", [`LogUp` argument], <logup>),
13+
("memory.typ", [Memory argument], <memory>),
14+
)),
15+
("OVERVIEW", (
16+
("variables.typ", [Variables], <vars>),
17+
("signatures.typ", [Signatures], <signatures>),
18+
)),
19+
("TEMPLATES", (
20+
("is_bit.typ", [`IS_BIT` template], <isbit>),
21+
("sign.typ", [`SIGN` template], <sign>),
22+
("add.typ", [`ADD`/`SUB` template], <add>),
23+
("neg.typ", [`NEG` template], <neg>),
24+
)),
25+
("MEMORY", (
26+
("memw.typ", [`MEMW` chip], <memw>),
27+
)),
28+
("CPU", (
29+
("decode.typ", [`DECODE` table], <decode>),
30+
("cpu.typ", [`CPU` chip], <cpu>),
31+
)),
32+
("ALU", (
33+
("shift.typ", [`SHIFT` chip], <shift>),
34+
("branch.typ", [`BRANCH` chip], <branch>),
35+
("lt.typ", [`LT` chip], <lt>),
36+
("mul.typ", [`MUL` chip], <mul>),
37+
("dvrm.typ", [`DVRM` chip], <dvrm>),
38+
("load.typ", [`LOAD` chip], <load>),
39+
("bitwise.typ", [`BITWISE` chips], <bitwise>),
40+
)),
41+
("ECALLS", (
42+
("about_ecalls.typ", [About `ECALL`], <ecall>),
43+
("halt.typ", [`HALT` chip], <halt>),
44+
("commit.typ", [`COMMIT` chip], <commit>),
45+
))
46+
)
47+
)
48+
#let meta_sections = meta.summary.map(m => m.at(1)).sum()
49+
#book-meta(
50+
title: meta.title,
51+
authors: meta.authors,
52+
summary: prefix-chapter("front.typ", meta.title)
53+
+ meta.summary.map(
54+
((title, sections)) => {
55+
heading(depth: 1, title) + sections.map(((ch, title, _ref)) => chapter(ch, title)).join()
56+
}
57+
).join()
58+
)
59+
60+
#let common-formatting(body) = {
61+
set footnote(numbering: "[1]")
62+
show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt)
63+
body
64+
}
65+
66+
67+
#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[
68+
#set text(fill: foreground)
69+
*TODO #if name != none { [(#name)] }*: #body
70+
]
71+
#let rj = todo.with(background: teal, name: "Robin")
72+
#let et = todo.with(background: rgb("d4aa3a"), name: "Erik")
73+
#let cdsg = todo.with(background: olive, name: "Cyprien")
74+
75+
#let aside(title, body) = context figure(
76+
block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false)[
77+
#block(inset: (left: 1em, right: 1em, top: .75em, bottom: .75em),
78+
width: 100% + 2em,
79+
fill: rgb("55aaff"),
80+
stroke: luma(50%),
81+
align(center, strong(text(fill: black, title))))
82+
#align(left, body)
83+
])
84+
85+
86+
#let is-shiroa = "x-target" in sys.inputs
87+
88+
// Strip styling to keep only "pure" content.
89+
// This is useful to avoid errors on the `set document(...)` in `project`
90+
// when invisibly including other chapters to resolve xrefs.
91+
#let strip-all(content) = {
92+
if repr(content.func()) == "sequence" {
93+
for c in content.children {
94+
strip-all(c)
95+
}
96+
} else if repr(content.func()) == "styled" {
97+
strip-all(content.child)
98+
} else {
99+
content
100+
}
101+
}
102+
103+
#let _toplevel = state("_toplevel", none)
104+
#let _xref-included = state("_xref-included", (:))
105+
106+
// Invisibly include another chapter, so that its labels can be resolved
107+
#let xref-include(f) = {
108+
context {
109+
place(hide(box(width: auto, height: 0%, strip-all(include "/" + f))))
110+
}
111+
}
112+
113+
// Generate a cross-link for references to other chapters.
114+
// Leaves the ref untouched if it can't be resolved or points to the current chapter.
115+
#let xref(rf) = {
116+
assert(is-shiroa, message: "xref should only be used when compiling for shiroa")
117+
let lbl = rf.target
118+
let found = meta_sections.find(((_, _, tag)) => str(lbl).starts-with(str(tag)))
119+
context if found != none and found.at(0) != _toplevel.final() {
120+
let (ch, title, ref) = found
121+
if ref == lbl {
122+
cross-link("/" + ch, [Chapter #(meta_sections.position(x => x == found) + 1)])
123+
} else {
124+
// Because shiroa does weird url escaping
125+
let shiroa-label = label(str(lbl).replace(":", "%3A"))
126+
context _xref-included.update(x => x + ((ch): true))
127+
// The ideal would be to use `rf` directly as content argument to `cross-link`,
128+
// as that would inherit any/all formatting of the ref we want or need.
129+
// Unfortunately the ref link seems to take precedence over the cross-link hyperlink
130+
// when clicking.
131+
// There may still be some way around it by messing with some html output
132+
let link-content = context {
133+
let fig = query(lbl).first()
134+
let counter = if fig.has("counter") {
135+
fig.counter
136+
} else {
137+
counter(fig.func())
138+
}
139+
140+
let supplement = if rf.supplement == auto {
141+
fig.fields().at("supplement", default: none)
142+
} else {
143+
rf.supplement
144+
}
145+
[#supplement#numbering(fig.numbering, ..counter.at(lbl))]
146+
}
147+
cross-link("/" + ch, reference: shiroa-label, link-content)
148+
}
149+
} else {
150+
rf
151+
}
152+
}
153+
154+
#let book-page(file, ..args) = {
155+
if not file.ends-with(".typ") {
156+
file = lower(file) + ".typ"
157+
}
158+
159+
assert(meta_sections.find(s => s.at(0) == file) != none, message: "Couldn't resolve typst source file " + file)
160+
161+
if is-shiroa {
162+
(body) => {
163+
show: common-formatting
164+
context _toplevel.update(s => {
165+
if s == none {
166+
file
167+
} else {
168+
s
169+
}
170+
})
171+
let cond() = _toplevel.final() == file
172+
project.with(..args, title: context meta_sections.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([
173+
#show ref: it => context if _toplevel.final() == file {
174+
xref(it)
175+
}
176+
#context _xref-included.final().pairs().map(((key, value)) => context if value and cond() {
177+
xref-include(key)
178+
}).join()
179+
#body
180+
])
181+
}
182+
} else {
183+
body => body
184+
}
185+
}

spec/branch.typ

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
#import "/book.typ": book-page, rj
2+
#import "/src.typ": load_config, load_chip
3+
#import "/chip.typ": (
4+
render_chip_assumptions,
5+
render_chip_variable_table,
6+
compute_nr_interactions,
7+
total_nr_variables,
8+
total_nr_instantiated_columns,
9+
render_constraint_table,
10+
render_chip_padding_table,
11+
)
12+
13+
#let config = load_config()
14+
#let chip = load_chip("src/branch.toml", config)
15+
16+
#show: book-page(chip.name)
17+
#let branch = raw(chip.name)
18+
19+
The #branch chip computes the target address of a branching instruction.
20+
21+
= Variables
22+
#let nr_variables = total_nr_variables(chip)
23+
#let nr_columns = total_nr_instantiated_columns(chip, config)
24+
#let nr_interactions = compute_nr_interactions(chip)
25+
26+
The #branch chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
27+
#render_chip_variable_table(chip, config)
28+
29+
= Assumptions
30+
31+
#render_chip_assumptions(chip, config)
32+
33+
= Constraints
34+
35+
We constrain `next_pc` to be $#`base_address` + #`offset`$,
36+
where `base_address` equals `pc` when $#`JALR` = 0$ and `register` otherwise.
37+
38+
The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed implicitly by the `AND_BYTE` lookup.
39+
#render_constraint_table(chip, config, groups: "all")
40+
41+
This chip contributes the following to the lookup argument.
42+
#render_constraint_table(chip, config, groups: "output")
43+
44+
= Padding
45+
46+
The table can be padded to the next power of two with the following value assignments:
47+
48+
#render_chip_padding_table(chip, config)

0 commit comments

Comments
 (0)