spec v0.2

.github/workflows/pr_spec.yaml

@@ -0,0 +1,25 @@
+name: Spec tests
+on:
+  pull_request:
+    branches:
+      - main
+      - 'spec/**'
+  push:
+    branches: ["**"]
+    paths: ["spec/**"]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  spec_structure:
+    name: Spec structure test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions/setup-python@v6
+      - run: python3 spec/tooling/chip.py spec/src/config.toml spec/src/signatures.toml spec/src/*.toml

spec/.editorconfig

@@ -0,0 +1,10 @@
+root = true
+
+[*]
+end_of_line = lf
+insert_final_newline = true
+charset = utf-8
+
+[*.typ]
+indent_style = space
+indent_size = 2

spec/.gitignore

@@ -0,0 +1,2 @@
+dist/*
+ebook.pdf

spec/README.md

@@ -0,0 +1,11 @@
+# LambdaVM specification
+This repository contains specification for [`LambdaVM`](https://github.com/yetanotherco/lambda_vm).
+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).
+
+## Installation & Development setup
+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. Clone this repository.
+4. Open the repository in a terminal and execute `shiroa serve`.
+
+At this point, the wiki version is hosted locally and is actively updated as you modify the specification files.

spec/about_ecalls.typ

@@ -0,0 +1,24 @@
+#import "/book.typ": book-page, aside
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_variable_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  render_constraint_table,
+  render_chip_assumptions,
+  render_chip_padding_table,
+)
+
+#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:
+- register `A7` contains the system call number
+  #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]]]),
+- the arguments are located in registers `A0`-`A6`, and
+- the return value is written to `A0`,
+where `A0`-`A7` are symbolic names for the registers `x10`-`x17`
+#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

@@ -0,0 +1,33 @@
+#import "/book.typ": book-page, 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)
+
+#show: book-page(chip.name)
+
+#set_nr_interactions(chip, name: "SUB")
+#let nr_interactions = compute_nr_interactions(chip)
+
+#let add = raw(chip.name)
+#let sub = raw("SUB")
+
+#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.
+For ease of notation, we moreover introduce the #sub constraint template
+$
+#`SUB<diff; lhs, rhs>` := #`ADD<lhs; rhs, diff>`,
+$
+in both conditional and unconditional versions.
+It constrains that $#`diff` equiv #`lhs` - #`rhs` (mod 2^64)$ when the expression `cond` is non-zero.
+
+= Variables
+This template introduces #nr_interactions interaction(s).
+#render_chip_variable_table(chip, config)
+
+= Assumptions
+#render_chip_assumptions(chip, config)
+
+= Constraints
+This template introduces the following constraints
+#render_constraint_table(chip, config)

spec/bitwise.typ

@@ -0,0 +1,45 @@
+#import "/book.typ": book-page, rj
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_assumptions,
+  render_chip_variable_table,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  render_constraint_table,
+)
+
+#let config = load_config()
+#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
+and convenience functionalities over small domains.
+
+= Variables
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_precomputed = ("input", "output").map(c => chip.variables.at(c)).flatten().len()
+
+The #bitwise chip is comprised of #nr_variables variables that are expressed using #nr_columns columns.
+Of these, the _input_ and _output_ variables (#nr_precomputed in total) are precomputed.
+#render_chip_variable_table(chip, config)
+
+*Note*: This table contains one row for every possible value of `(X, Y, Z)`.
+As such, it has length $2^8 dot 2^8 dot 2^4 = 2^(20)$.
+
+= Lookup
+This chip adds the following interactions to the lookup:
+#render_constraint_table(chip, config)
+
+= Notes/Optimizations
+The following ideas may prove to be optimizations for the #bitwise chip:
++ Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once. 
+  When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`.
++ Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8<X> := MSB16[256X]`.
+  Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`).
+  This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check.
++ Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, etc.) and 20-bit (`HWSL`, `IS_B20`, `ZERO`) lookups in separate tables.

spec/book.typ

@@ -0,0 +1,185 @@
+#import "@preview/shiroa:0.3.1": *
+#import "/templates/page.typ": project
+
+#show: book
+
+#let meta = (
+  title: "Lambda VM specification",
+  authors: ("3MI Labs", "Aligned"),
+  version: "0.2",
+  summary: (
+    ("PROOF SYSTEM", (
+        ("logup.typ", [`LogUp` argument], <logup>),
+        ("memory.typ", [Memory argument], <memory>),
+    )),
+    ("OVERVIEW", (
+        ("variables.typ", [Variables], <vars>),
+        ("signatures.typ", [Signatures], <signatures>),
+    )),
+    ("TEMPLATES", (
+      ("is_bit.typ", [`IS_BIT` template], <isbit>),
+      ("sign.typ", [`SIGN` template], <sign>),
+      ("add.typ", [`ADD`/`SUB` template], <add>),
+      ("neg.typ", [`NEG` template], <neg>),
+    )),
+    ("MEMORY", (
+      ("memw.typ", [`MEMW` chip], <memw>),
+    )),
+    ("CPU", (
+      ("decode.typ", [`DECODE` table], <decode>),
+      ("cpu.typ", [`CPU` chip], <cpu>),
+    )),
+    ("ALU", (
+      ("shift.typ", [`SHIFT` chip], <shift>),
+      ("branch.typ", [`BRANCH` chip], <branch>),
+      ("lt.typ", [`LT` chip], <lt>),
+      ("mul.typ", [`MUL` chip], <mul>),
+      ("dvrm.typ", [`DVRM` chip], <dvrm>),
+      ("load.typ", [`LOAD` chip], <load>),
+      ("bitwise.typ", [`BITWISE` chips], <bitwise>),
+    )),
+    ("ECALLS", (
+      ("about_ecalls.typ", [About `ECALL`], <ecall>),
+      ("halt.typ", [`HALT` chip], <halt>),
+      ("commit.typ", [`COMMIT` chip], <commit>),
+    ))
+  )
+)
+#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 common-formatting(body) = {
+  set footnote(numbering: "[1]")
+  show raw.where(block: true): it => block(it, inset: 1em, width: 100%, radius: 5pt)
+  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 aside(title, body) = context figure(
+  block(inset: (left: 1em, right: 1em, bottom: 1em), stroke: luma(50%), breakable: false)[
+    #block(inset: (left: 1em, right: 1em, top: .75em, bottom: .75em),
+           width: 100% + 2em,
+           fill: rgb("55aaff"),
+           stroke: luma(50%),
+           align(center, strong(text(fill: black, title))))
+    #align(left, body)
+])
+
+
+#let is-shiroa = "x-target" in sys.inputs
+
+// Strip styling to keep only "pure" content.
+// This is useful to avoid errors on the `set document(...)` in `project`
+// when invisibly including other chapters to resolve xrefs.
+#let strip-all(content) = {
+  if repr(content.func()) == "sequence" {
+    for c in content.children {
+      strip-all(c)
+    }
+  } else if repr(content.func()) == "styled" {
+    strip-all(content.child)
+  } else {
+    content
+  }
+}
+
+#let _toplevel = state("_toplevel", none)
+#let _xref-included = state("_xref-included", (:))
+
+// Invisibly include another chapter, so that its labels can be resolved
+#let xref-include(f) = {
+  context {
+    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
+      project.with(..args, title: context meta_sections.find(x => x.at(0) == _toplevel.final()).at(1), cond: cond)([
+        #show ref: it => context if _toplevel.final() == file {
+          xref(it)
+        }
+        #context _xref-included.final().pairs().map(((key, value)) => context if value and cond() {
+          xref-include(key)
+        }).join()
+        #body
+      ])
+    }
+  } else {
+    body => body
+  }
+}

spec/branch.typ

@@ -0,0 +1,48 @@
+#import "/book.typ": book-page, rj
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_assumptions,
+  render_chip_variable_table,
+  compute_nr_interactions,
+  total_nr_variables,
+  total_nr_instantiated_columns,
+  render_constraint_table,
+  render_chip_padding_table,
+)
+
+#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.
+
+= Variables
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+#let nr_interactions = compute_nr_interactions(chip)
+
+The #branch chip is comprised of #nr_variables variables that are expressed using #nr_columns columns and leverages #nr_interactions interaction(s):
+#render_chip_variable_table(chip, config)
+
+= Assumptions
+
+#render_chip_assumptions(chip, config)
+
+= Constraints
+
+We constrain `next_pc` to be $#`base_address` + #`offset`$,
+where `base_address` equals `pc` when $#`JALR` = 0$ and `register` otherwise.
+
+The range checks on `unmasked_low_byte` and `next_pc_low[0]` are performed implicitly by the `AND_BYTE` lookup.
+#render_constraint_table(chip, config, groups: "all")
+
+This chip contributes the following to the lookup argument.
+#render_constraint_table(chip, config, groups: "output")
+
+= Padding
+
+The table can be padded to the next power of two with the following value assignments:
+
+#render_chip_padding_table(chip, config)